veyepar: Usable formal methods - are we there yet?

Hi user

Admin Login:

Name: Usable formal methods - are we there yet?
--client lca --show lca2016 --room r3mix 10683 --force
Prev: 0 to be advised
Next: 12 Improving thread synchronization in GlusterD (Daemon for Gluster) using Userspace RCU (Read-copy-update)

show more...

Author(s):	Stefan Götz
Location	Wool Museum
Date	feb Wed 03	Days Raw Files
Start	11:35	First Raw Start	10:16
Duration	0:45:00	Offset	1:18:51
End	12:20	Last Raw End	12:21
Chapters	00:00 0:37:59
Total cuts_time	45 min.

https://linux.conf.au/schedule/30141/view_talk
raw-playlist raw-mp4-playlist encoded-files-playlist host archive tweet mp4 svg png

final audio

assets release.pdf Usable_formal_methods_are_we_there_yet.json
logs
Admin: episode episode list cut list raw files day marks day marks day image_files

State:
Locked:	clear this to unlock
Locked by:	user/process that locked.
Start:	initially scheduled time from master, adjusted to match reality
Duration:	length in hh:mm:ss
Name:	Video Title (shows in video search results)
Emails:	email(s) of the presenter(s)
Released:	has someone authorised pubication
Normalise:
Channelcopy:	m=mono, 01=copy left to right, 10=right to left, 00=ignore.
Thumbnail:	filename.png
Description:	Creating safe and secure software is hard, and counter-intuitively even harder in tiny embedded devices - devices that drive you, fly you, inject you with medicine, or keep your heart beating. We present how we have prevented bugs in embedded systems with open-source tools for formal methods. The big advantage of formal methods is that they can intercept bugs before code is built or run. Therefore, they avoid the difficulties of the classic approaches: testing, run-time checking, or re-using standard code. Our experience is based on static analysis with splint and model checking with CBMC for the eChronos real-time operating system. Safety-critical applications, such as UAV research and commercial medical devices rely on eChronos as their core OS. The formal methods tools are part of our development process and Continuous Integration system, so they help find bugs both in the OS itself and in the application code. This presentation shows how we apply splint and CBMC to real-world code and the practical lessons we have learned in the process. This includes: - a brief overview of the fundamental strengths and weaknesses of each approach and tool - the bugs we have found and the classes of bugs the tools prevent - how to apply the tools to a code base in practice, what is needed to support the tools, and how to maintain that support - the scalability and some limitations and bugs of the tools themselves, and where theory and practice do not line up - how such tools and formal methods in general can influence software design (which is usually to the better) Overall, formal methods have matured to be practical and valuable for real-world code in a real-world development process. The available open-source tools may require a design or code tweak here or there, but are well past purely academic relevance. markdown
Comment:	production notes

recording sheet

recording sheet

2016-02-03/10_16_09.dv Apply: 11:24:40 - 11:36:00 ( 00:11:20 ) S: 10:16:09 - E: 11:36:00 D: 01:19:51 (Start: 4111.0) show more...

vlc ~/Videos/veyepar/lca/lca2016/dv/r3mix/2016-02-03/10_16_09.dv :start-time=04111.0 --audio-desync=0

	Raw File	Cut List
	10:16:09		seconds: 4111.0 Wall: 11:24:40
Duration	01:19:51
	11:36:00		seconds: 0.0 Wall: 10:16:09
Comments:
mp4 mp4.m3u	dv.m3u	Split: Sequence:: delete

audio viz

2016-02-03/11_35_57.dv Apply: 11:36:00 - 12:14:00 ( 00:37:59 ) S: 11:35:57 - E: 12:14:00 D: 00:38:03 (Start: 3.1068) show more...

vlc ~/Videos/veyepar/lca/lca2016/dv/r3mix/2016-02-03/11_35_57.dv :start-time=03.1068 --audio-desync=0

	Raw File	Cut List
	11:35:57		seconds: 3.1068 Wall: 11:36:00
Duration	00:38:03
	12:14:00		seconds: 0.0 Wall: 11:35:57
Comments:
mp4 mp4.m3u	dv.m3u	Split: Sequence:: delete

audio viz

2016-02-03/12_13_59.dv Apply: 12:13:59 - 12:21:04 ( 00:07:05 ) S: 12:13:59 - E: 12:21:04 D: 00:07:05 show more...

vlc ~/Videos/veyepar/lca/lca2016/dv/r3mix/2016-02-03/12_13_59.dv :start-time=00.0 --audio-desync=0

	Raw File	Cut List
	12:13:59		seconds: 0.0 Wall: 12:13:59
Duration	00:07:05
	12:21:04		seconds: 0.0 Wall: 12:13:59
Comments:
mp4 mp4.m3u	dv.m3u	Split: Sequence:: delete

audio viz

Rf filename:	root is .../show/dv/location/, example: 2013-03-13/13:13:30.dv
Sequence:
get this:	check and save to add this

2016-02-03/10_16_09.dv
audio viz

audio viz

2016-02-03/11_35_57.dv
audio viz

audio viz

2016-02-03/12_13_59.dv
audio viz

audio viz

Veyepar Video Eyeball Processor and Review