Slide 1:Ed Brinksma Dept. of CS, University of Twente, NL joint work with Angelika Mader Monterey Workshop 2003 Chicago Verification Modelling of Embedded systems


ES Verification Example: storm surge barrier control :September, 2003 Monterey Workshop, Chicago ES Verification Example: storm surge barrier control


The control system :September, 2003 Monterey Workshop, Chicago The control system no human intervention human operation too unreliable responsible for closing & opening online meteorological & hydrological data very low failure rates event failure rate ~10-5/barrier event design & verification with FM considered successful


Design validation :September, 2003 Monterey Workshop, Chicago Design validation data types & operations formally specified in Z crucial control parts modelled in Promela & model checked with Spin implementations were hand-coded using Z specs implementations were tested no actual code was proved correct


Questions :September, 2003 Monterey Workshop, Chicago Questions How to do practical verification of ES ? Is it methodologically sound? How should this affect research?


The Setting :September, 2003 Monterey Workshop, Chicago The Setting verification of ES designs is desirable critical aspects are common: safety-critical, high replication, costly, etc. verification needs formalization operational model, logical theory, requirements formalization is problematic the (standard) combinatorial explosion incorporation of (physical) environment


Typical Situation :September, 2003 Monterey Workshop, Chicago Typical Situation verification model is constructed in an ad hoc and opportunistic manner the success of verification is crucially dependent on scarce expertise the relation of the verification model to the actual design is opaque the verification crisis: model hacking precedes model checking


What do we need? :September, 2003 Monterey Workshop, Chicago What do we need? Verification models should have/be limited complexity must be open to computer-aided verification faithful must capture relevant properties traceable clear relation to actual design or system


Complexity Issues :September, 2003 Monterey Workshop, Chicago Complexity Issues models must be sufficiently small limited capacity verification tools limited capacity verification management hybrid nature ES complicates models mixed techniques, symbolic analysis tool capacity growth exceeds Moore’s law better algorithms & data structures


Abstractions :September, 2003 Monterey Workshop, Chicago Abstractions Verification models are abstractions: inherent abstractions mathematical modelling of physical aspects controlled abstractions simplifications reducing complexity


Faithfulness :September, 2003 Monterey Workshop, Chicago Faithfulness Verification of erroneous models is useless (or even worse). Models must obviously capture the relevant system properties. However: what are relevant (formal) properties? these are often part of the design problem do our abstractions preserve them? this can be difficult to show (begging the question) verification models & properties must be validated !


Model validation :September, 2003 Monterey Workshop, Chicago Model validation In addition to traceability verification models can be validated by experimental means: simulation of the model requires constructive modelling analysis of verification results in practice model validation and verification are mixed


Separating the errors :September, 2003 Monterey Workshop, Chicago Separating the errors a verification run may fail due to an error in the implementation an error in the verification model an error in the formal property errors must be analysed to modify appropriate entity requires rigourous protocol for analysis & documentation verification should always include a systematic error discussion (cf. physics)


Software Model Extraction :September, 2003 Monterey Workshop, Chicago Software Model Extraction program code as model reduction by abstract interpretation data/predicate abstraction variable slicing model check abstractions eliminate false negatives does not work for non-programmable model parts


Verification Engineering :September, 2003 Monterey Workshop, Chicago Verification Engineering Verification modelling as a design problem closely related but different from system design main design criterion: limited complexity & tool support Systematic approach to model construction capture physical aspects reduce complexity formal and experimental justification Tool support for verification management model/property version management meta-level specification of verification campaigns


Systematic Verification Model :September, 2003 Monterey Workshop, Chicago Systematic Verification Model interpret error


Xspin/Project - usage :September, 2003 Monterey Workshop, Chicago Xspin/Project - usage “Sandbox” environment: Accessing PRCS Saving validation results Forcing version integrity


Challenges :September, 2003 Monterey Workshop, Chicago Challenges verification methodology (MoMS project) systematic model traceability combining formal and non-formal aspects modelling & abstraction patterns libraries, domain dependent solutions systematic model validation verification management tools documentation & version control verification integrity control verification campaign management


And finally … :September, 2003 Monterey Workshop, Chicago And finally … the company involved got very enthusiastic about FM a 1-year technology transfer project was carried out after 5 years they are still only using the (model-driven) testing tools