Name
Abstract | ||
|---|---|---|
Modern reactive control system are typically very complex entities, and their design poses substantial challenges. In addition to ensuring functional correctness, other steps may be required: with safety analysis, the behavior is analyzed, and proved compliant to some requirements considering possible faulty behaviors; diagnosis and diagnosability are forms of reasoning on the run-time explanation of faulty behaviors; planning and synthesis allow the automated construction of controllers that implement desired behaviors. Symbolic Model Checking (SMC) is a formal technique for ensuring functional correctness that has achieved a substantial industrial penetration in the last decade. In this paper, we show how SMC can be used as a convenient framework to express safety analysis, diagnosis and diagnosability, and synthesis. We also discuss how model checking tools can be used and extended to solve the resulting computational challenges. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/978-3-540-74128-2_1 | MoChArt |
Keywords | Field | DocType |
substantial industrial penetration,functional correctness,possible faulty behavior,faulty behavior,safety analysis,symbolic model checking framework,substantial challenge,symbolic model checking,complex entity,computational challenge,automated construction,model checking | Kripke structure,Computation tree logic,Model checking,Computer science,Correctness,Theoretical computer science,Linear temporal logic,Reactive control | Conference |
Volume | ISSN | Citations |
4428 | 0302-9743 | 5 |
PageRank | References | Authors |
0.61 | 41 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Piergiorgio Bertoli | 1 | 775 | 46.89 |
| Marco Bozzano | 2 | 743 | 49.82 |
| Alessandro Cimatti | 3 | 5064 | 323.15 |