CHARTER---Critical and High Assurance Requirements Transformed through Engineering Rigour

CHARTER-Critical and High Assurance Requirements Transformed through Engineering Rigour

Funding Agency: European Union Framework 7, ARTEMIS-2008-1

Start date: 1 April 2009

Duration: 36 months

Summary

Today, embedded software systems assist, accelerate, and control various aspects of European society. They enable businesses to perform better and make citizen's lives more convenient. Just a few, especially such as for aircraft control and nuclear power supply, are critical to human life. This will change drastically.

Future generations will experience software pervasiveness that can hardly be imagined today. Embedded systems will literally be found everywhere and control almost everything. Human life will depend on software to an inconceivable extent. To protect our society from the resulting severe risks, ever more software will be subject to governmental regulations. Whenever software is deployed in sensitive applications, certification processes will be needed. The costly and time-consuming procedures employed today to verify new software, for example in the air flight industry, will fail to meet demands of this scale.

CHARTER will ease, accelerate, and cost-reduce the certification of critical embedded systems by melding Real-time Java, Model Driven Development, rule-based compilation, and formal verification. This approach, Quality-Embedded Development (QED), will push software certification to a new level and thereby significantly contribute to the safety and security of the upcoming age of an embedded software society.

Research Focus

The focus of Dr. Kiniry's work in CHARTER is Model-based Reasoning about Concurrency in RTSJ (the Real-Time Specification for Java).

RTSJ's concurrency semantics are much stronger than those of standard Java. In particular, the formal specification of threads is now possible as priorities and scheduling are a core part of the standard. Moreover, because of improvements made to the Java Memory Model (JSR 133) and the availability of high-level concurrency constructs (JSR 166), reasoning about multitasking programs at the model level is tractable.

Our work focuses on developing with highest priority a small set of native JML types focused on all of the low-level (i.e., locks, blocks, monitors, and threads), and some of the key high-level concurrency constructs available in Real-Time Java. These native JML types will be mechanically formally specified in such a way that reasoning about existing current Safety-Critical Java code can be performed primarily, and perhaps exclusively, at the model level.

Moreover, leveraging existing work in UTP will then enable the specification and verification of the concurrent facets of a system using appropriate formalisms and tools (e.g., model checkers for formal frameworks like CSP, UNITY, and UPPAAL) to support the automatic generation of fully annotated, well documented, verifiable source code.

The mandatory sub-tasks of this task include: (1) the high-level specification of the core concurrency constructs of RTSJ (as mentioned above) in both JML and in a mechanical theorem prover, (2) provide a formal method with tool support for reasoning about these high-level constructs based upon existing work in reasoning about concurrent Java (as accomplished, in part, by CHARTER participants Chalmers and Nijmegen as part of the FP6 project "Mobius"), and (3) specifying and verifying the implementation and use of the most commonly used high-level concurrency classes from JSR 166 used in RTSJ systems.

The secondary sub-task is (4) reusing an existing concurrency formalization methodology and tool-set (e.g., CSP and FDR) to generate concurrent Java code with formal annotations that is easily verified using the results of (1)-(3).

Deliverables

D6.3: JML Model for Real-time Concurrency (month 18)
A set of JML models formalizing key concurrency constructs in Safety-Critical Java (SCJ). Formal JML model-based specifications will be written and checked for correctness for the typical set (i.e., cover the standard use cases seen in practice) of concurrency constructs used in SCJ. We will identify this typical set through the static analysis of the design and implementation of a large body of existing SCJ software. Each module specification will cover the entire public interface of the class or interface in question and its utility will be measured in terms of its verification efficiency with respect to the concurrency checker of D6.4.
D6.4: A Concurrency Checker (month 24)
A prototype checker for checking safety and liveness concurrency properties of Real-time Java programs annotated with JML mode-based specifications produced by D6.3. This checker will have both a static/automatic and a dynamic/interactive mode of operation, as appropriate for the verification and resources on-hand. It will leverage existing tools (e.g., generic and concurrency theory-specific model checkers, the JML tool suite, Mobius tools, etc.) for reasoning about concurrent models as well as incorporate new, novel techniques (e.g. speculatively, automatic decision procedures for concurrent separation logic). The concurrency checkers utility will be measured in terms of the differential in verification code coverage obtained for the CHARTER case studies that involve concurrency.