1. Formal methods and related tools can be used most profitable to analyse parts of systems that are most critical. The development of guidelines for the identification of those system parts, the level of formality that is required and the selection of the most appropriate method to analyse its properties need to be addressed.
2. The development of convenient and powerful logics to express relevant quantitative dependability measures in a precise, concise and formal way is key to future systematic and possible automatic, analysis of dependability aspects of critical systems. The development of logics to express in addition cost and reward based measures can greatly enhance the number of interesting measures relevant for dependable systems.
3. Counterexamples generated by model checkers provide designers with valuable information about possible problems in their designs. The extension of these examples to quantitative model checking for performance and dependability aspects of designs is one of the key issues that need to be addressed.
4. The efficiency and effectiveness of Model Checking for Performance and Dependability evaluation depends critically on the development of suitable, possibly automated, abstraction mechanisms in order to deal with very large state spaces.
5. Particular attention must be paid to the development of models that can take user interaction with the system into account. Also here quantitative models play an important role when it comes to descriptions of human performance aspects relevant for the overall evaluation of critical systems.
6. The use of different methods brings about the issue of the relation between models used for different verification purposes (e.g. simulation models, models used for model checking and theorem proving but also formalisms used for data intensive vs. those for control intensive problems). This becomes particularly relevant in the case of combined verification.
7. Training of designers, integration of tools and methods in the design process and the development of course ware to allow a broad take-up of formal methods in industry and elsewhere are fundamental for the transfer of available knowledge to the daily practice of software developers.
Defines standard
Replaced/Superseded by document(s)
Cancelled by
Amended by
| File | MIME type | Size (KB) | Language | Download | |
|---|---|---|---|---|---|
| A Dependability Roadmap.pdf | application/pdf | 230.06 KB | English | DOWNLOAD! |
Provides definitions
Cover images
Introduction
The class of systems that require the application of the most effective and rigorous quality control measures are those with high technical complexity where management of concurrent, distributed, real-time activities in presence of faults or other rare combinations of events is critical.
This combination of factors is likely to be found in an increasing number of critical hardware and software systems as a consequence of the inevitable grow in scale and functionality and the trend to interconnect systems in networks. The likelihood of subtle, difficult to detect errors in this class of systems is much greater than in systems without concurrency and real time requirements, in particular if also human interaction with the system is considered.