CHARTER (ARTEMIS)

Purpose and goal

This project will improve the software development of critical systems in three main areas: rule based transformation systems for MDD code generation and certifiable compilation, advancing deductive verification methods for more powerful verification and requirements driven testing, and extending requirement engineering for object oriented systems. Techniques will be developed to reduce the need for test by relating the code coverage provided by formal verification with testing. A multilevel certification paradigm will be developed to reduce the cost of certifying complex systems while raising the confidence in the resulting system. Realtime Java is an essential ingredient for this development due to the languages clean syntax and semantics and support for garbage collection.

Results and expected effects

The CHARTER project will have a substantial impact in improving the costs for critical embedded systems software developed. Specific objectives that have been established for the project are summarised below: Reduce design time - Time from requirements to running code - 20% reduction in design time Increase reuse - Classes that can be taken from one project to another - 30% increase in reusable classes Reduce platform porting effort - Coding and validation time needed to change platform - 35% reduction in porting effort Improve use of formal methods - Minimize errors found during testing - 20% reduction in errors reported during test phase Reduce test generation effort - Time needed to generate tests - 25% reduce in time required to generate test cases

Approach and implementation

The CHARTER project will use realtime Java to both improve on the existing safety critical design process and make the process more accessible outside the current safety-critical domain. By taking advantage of past advances in realtime Java, development can focus on pushing safety-critical design beyond the current state of the art. Formal methods will be used to improve all aspects of the design process from code generation to resource analysis and the determination of application correctness. The goal is to provide a new paradigm for Quality Embedded Development (QED). CHARTER will focus on using formal methods to improve the safety critical development process yielding several important innovations. These innovations will help master system complexity by allowing cost effective mapping of applications and product variants onto embedded platforms. Using formal methods will enable the resultant designs to respect constraints concerning resources (time, memory, etc.), safety, security, and quality of service.