Model based development is an attractive approachin systems and software where time to market is critical anddevelopment cycles are short. This approach is increasingly relevant tosafety critical systems.
|Figure1: SCADE design model|
In model based development explicit graphicalmodels are used to define and describe a system. This approach isattractive because:
- Developers can test and analyse their system before any code iswritten.
- Models are expressed in notations that are easily understood,supporting communication between systems and software engineers
Within safety critical software development thereare additional requirements that a model based development has to takeinto account; freedom from ambiguity and determinism. These are areaswhere the model based process can fail.
This article uses SCADE (Safety Critical Application DevelopmentEnvironment), a tool that supports model based development and safecode generation, to discuss how the problems of determinism andambiguity can be addressed resulting in an implementation view of thecontrol model.
SCADE is a graphical modelling tool in whichengineers can specify a control model using familiar block diagrams andstate diagrams, simulate and generate safe production code forembedding. Figure 1 above shows an example of a SCADE design.
Freedom from ambiguity
Systems engineers develop quantitative models to describecontrol algorithms. These are typically block diagrams or statemachines (Figure 2 below ).
|Figure2. SCADE modeling sub-set|
Verification of the control model is achievedthrough simulation in a design environment. Implementation choices aremade for the software simulation through simulation settings, implicitsampling rates or the graphical position of model elements.
This assists efficiency as the systems engineers donot concern themselves with detail outside the scope of preciselydefining control laws.
Software engineers develop models that describearchitectural, structural and behavioural aspects of the software. Theytypically reference control law algorithms from the systems engineeringenvironment. However it may not be clear to a software engineer theimplicit assumptions that the control model was built on.
Therefore it is easy for software engineers to makeincorrect assumptions about model behaviour. If the software is basedupon different assumptions from those of the control model then thebehaviour of the software will diverge from the required behaviour ofthe model. The control model is precise from the system engineers pointof view, but ambiguous from the software engineers point of view.
SCADE is based on a formal graphical language. Thelanguage was defined in close connection with its early industrialusers and certification authorities in the aeronautics domain.
Formal specifications sit behind all the diagramsdeveloped in SCADE. These specifications are sequences of equationsthat provide an unambiguous meaning for the model. Therefore,interpretation of SCADE models does not depend on hidden settings, toolversion or graphical positioning.
SCADE provides a number of options for modelvalidation before software development has completed:
- can be simulated with system level scenarios. SCADE�½s codegenerator enables system software simulation. At a source level yoursimulation is the same as the software that you embed.
- Models can be exported and simulated in tools outside of SCADE.For example if Simulink? is used then the code generated by SCADE maybe exported as an S-Function to allow re-running of system scenarios.
- Formal proofs can be constructed across the model. Testingtypically shows correctness only for the values used in the tests.Formal proof shows correctness over the whole input space. Anexhaustive way to demonstrate that safety properties hold over thewhole system.
Safety-critical software must be deterministic. Control modelsdeveloped for system rapid prototyping are typically non-deterministic.For example within a state machine the control model may run until allpossible transitions have been taken.
One of the challenges of safety critical softwareis to translate non-deterministic specification behaviour into bounded,deterministic behaviour. However, this translation may cause thesoftware implementation to diverge from the control model behaviour.
To meet the goals of model based softwaredevelopment, where a design model can be exercised early in thedevelopment, there is a need to incorporate architectural constraintsinto the control model to reflect the translation decisions.
SCADE automatically incorporates constraints thatensure deterministic behaviour of the control model. A SCADE model hasthe following features that ensure predictable steady execution timeand memory use on the target:
- Safe control structures and linear control sequences are employed(no recursion, no jumps, etc).
- A SCADE model is strongly typed; no dynamic variables, and fullystatic memory allocation ensure data integrity.
With SCADE control models can be developed which automatically takeinto account the constraints of a safety critical software development.The model can then be used directly to generate production code. SCADEtakes a central place in the whole system-software workflow.
The formal basis of SCADE, along with rigorousvalidation carried out on the tool, allows a high level of confidenceto be placed in the generated code. The validation evidence availablefor SCADE has allowed safety authorities to audit and �½certify�½ thetool so that the code it generates may be used with reduced unittesting requirements.
SCADE operates as a “Certified Software Factory”,providing the necessary tools to perform Verification and Validation(V&V) activities early in the development life cycle, atmodel-level.
With SCADE there is now a deterministic unambiguouscontrol model that takes into account a safe architecture. We canexecute it early in the design cycle, and we have a high degree ofconfidence that model and final software will operate in the same way.
PaulRaistrick is technical manager at Esterel Technologies .