Name
Abstract | ||
|---|---|---|
An increasingly large number of safety-critical embedded systems rely on software to prevent and mitigate hazards occurring due to design errors and unexpected interactions of the system with its users and the environment. Implementing a safety instrumented function in the way advocated by the traditional software methods requires an intimate understanding and thorough validation of a complex ecosystem of programming languages, compilers, operating systems and hardware. We propose to consider an alternative where a system designer, for each individual problem, creates in a correct-by-construction manner both the design of a system and its compilation and execution infrastructure. This permits an uninterrupted chain of a formal correctness argument spanning from formalised requirements all the way to the gate-level characterisation of an execution environment. The past decade of advances in verification technology turned the mechanical verification of large-scale models into a reality while the pressure of certification makes the cost of a formally verified development routine increasingly acceptable. The proposal fits the Grand Challenge for Computer Research posed by Hoare in 2003, namely, development of a Verifying Compiler which not only mechanically translates a given program from one language to another but also verifies its correctness according to a formal specification. This allows meeting the most stringent software certification requirements such as SIL 4. We illustrate the vision with a small case-study developed using the Event-B modelling notation and tools. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.7873/DATE.2014.100 | Design, Automation and Test in Europe Conference and Exhibition |
Keywords | Field | DocType |
embedded systems,formal specification,formal verification,operating systems (computers),program compilers,programming languages,safety-critical software,event-B modelling notation,execution infrastructure,formal correctness argument,formal specification,gate-level characterisation,hazard mitigation,large-scale models,mechanical verification technology,operating systems,programming languages,safety critical system design,safety instrumented function,safety-critical embedded systems,software certification,verifying compiler | Notation,Systems engineering,Life-critical system,Computer science,Correctness,Formal specification,Real-time computing,Compiler,Software,Certification,Formal verification | Conference |
ISSN | Citations | PageRank |
1530-1591 | 0 | 0.34 |
References | Authors | |
2 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alex Iliasov | 1 | 0 | 0.34 |
| Arseniy Alekseyev | 2 | 24 | 2.54 |
| Danil Sokolov | 3 | 227 | 27.50 |
| Andrey Mokhov | 4 | 136 | 26.57 |