Name
Abstract | ||
|---|---|---|
A fundamental problem in the design and development of embeddedcontrol systems is the verification of safety requirements. Formal methods,offering a mathematical way to specify and analyze the behavior of asystem, together with the related support tools can successfully beapplied in the formal proof that a system is safe. However, the complexityof real systems is such that automated tools often fail to formallyvalidate such systems.This paper outlines an experience on formal specification andverification carried out in a pilot project aiming at the validation of arailway computer based interlocking system. Both the specification and theverification phases were carried out in the JACK (Just Another ConcurrencyKit) integrated environment. The formal specification of the system was doneby means of process algebra terms. The formal verification of the safetyrequirements was done first by giving a logical specification of such safetyrequirements, and then by means of model checking algorithms. Abstractiontechniques were defined to make the problem of safety requirementsvalidation tractable by the JACK environment. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1023/A:1008645826258 | Formal Methods in System Design - Special issue: industrial critical systems |
Keywords | Field | DocType |
safety critical systems,mechanical verification,temporal logic,model checking | Specification language,Computer science,Real-time computing,Formal specification,Verification,Runtime verification,Refinement,Formal methods,System requirements specification,Formal verification | Journal |
Volume | Issue | ISSN |
12 | 2 | 1572-8102 |
Citations | PageRank | References |
30 | 1.86 | 25 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cinzia Bernardeschi | 1 | 226 | 31.87 |
| Alessandro Fantechi | 2 | 1199 | 103.40 |
| Stefania Gnesi | 3 | 1475 | 120.93 |
| Salvatore Larosa | 4 | 47 | 3.34 |
| Giorgio Mongardi | 5 | 69 | 6.34 |
| Dario Romano | 6 | 70 | 6.28 |