(no subject)

Date: 2013-06-28 07:55 am (UTC)
purplecat: Hand Drawn picture of a Toy Cat (mathematics)
From: [personal profile] purplecat
It's the first. Model checking works a bit like exhaustive path coverage testing. So, for instance, if you have a multi-threaded program it will explore all possible thread-interleavings and make sure you have no deadlocks anywhere. Obviously it has massive issues with efficiency (and even feasibility).

It's called model checking because, outside a few fairly modern systems like Java pathfinder, you couldn't apply it to actual code, you had to create a model of your algorithm or protocol in the input language of the checker. Even with "program model checkers" such as Java Pathfinder, any time you have to worry about what a user will do, or parts of the overall system that aren't written in Java you basically have to model that part of the program in Java and then you test that the code works correctly in that model (but not necessarily in the real world).

One of the things we are pushing with the aircraft modelling, is working with the aircraft industry and certification authorities in the UK to attempt to agree on how Unmanned Aircraft should be certified for use in UK civilian airspace. One idea is that you restrict your verification results purely to the code part - so you prove things like "Assuming the sensor input is correct, the program will activate the right controls (even if those controls are broken and don't do what they should)" but the certification authorities (and aircraft manufacturers and designers - to be fair) really want the end results to be probabilistic estimates of the chance of catastrophic failure - so we want to be able to combine experimental results about the accuracy of sensors and the reliability of actuators with verification results about what actuators the program will use given which sensor inputs in order to generate an overall estimate of the chance of failure.
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
Account name:
If you don't have an account you can create one now.
HTML doesn't work in the subject.


If you are unable to use this captcha for any reason, please contact us by email at support@dreamwidth.org

Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.


purplecat: Hand Drawn picture of a Toy Cat (Default)

April 2019

 1 234 5 6
7 8 91011 12 13
14 15 16 17 18 19 20


Style Credit

Expand Cut Tags

No cut tags