The L4.verified Project and Its Next Steps
Timing Analysis of Embedded Software Systems
Embedded software is often applied in safety-criticial systems, e.g.
the braking system of a car or the steering gear of an airplane. Many
of these safety-critical systems are also time-critical, meaning that
the calculations performed by the tasks of the embedded system need not only be functionally correct but must be carried out in a timely
fashion. In this talk we show how real-time model checking using the
verification tool UPPAAL (www.uppaal.com) may be used to give such
timing guarantees. Clousot: Language agnostic static contract checking via abstract interpretation Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs.
CodeContracts take the form of preconditions, postconditions, and object invariants expressed as library calls. In the talk, I will introduce and demo
CodeContracts, the runtime checker, and I will describe the static
checker (Clousot), and the rationale behind its design. The CodeContracts API is part of .NET 4.0. The tools can be downloaded
here. |
Programme >