Name
Abstract | ||
|---|---|---|
Hybrid systems are at the core of most embedded and many other kinds of systems; formal methods for analysis of hybrid systems have made remarkable progress in the last decade and thus provide a strong foundation for assurance in the system core. But there are many systems issues that interact with the hybrid systems core and complicate the overall system design and its assurance case. These include real time and fault tolerance, interaction with human operators, and the relationship between verification and certification. For example, fault tolerance demands multiple redundant sensors, which are themselves prone to faults and inaccuracy, and whose precision degrades as real time progresses from the moment when the sample was taken to that when it is used. Fault tolerance generally also requires multiple independent channels of computation and this raises issues of their synchronization and coordination. There are two broad classes of methods for dealing with these combined issues: one uses architectural means to separate them, so we can reason separately about hybrid control and fault tolerance, for example; the other integrates them, so that a single method is used to reason, for example, about real time and fault tolerance. I decribe some of these methods and sketch some topics for further research. In the larger systems context, the embedded core may be managed by a planning and execution system that uses AI techniques, and/or by a human operator. Both of these may have an imperfect model of the system and incomplete knowledge of its internal state. I outline these topics and some of the interesting research opportunities therein. Finally, many of the systems we consider have the potential to do harm, and thus raise concern for informal or regulated certification. I outline recent developments in this area and their connection to verification. The rich relationship between hybrid systems and everything else suggests a need to reason cooperatively across multiple domains. I sketch a proposal for “an evidential tool bus” to facilitate this. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11730637_3 | HSCC |
Keywords | Field | DocType |
hybrid system,system design,fault tolerant,real time,formal method | Synchronization,Computer science,Systems design,Real-time computing,Fault tolerance,Operator (computer programming),Formal methods,Certification,Hybrid system,Distributed computing,Sketch | Conference |
ISBN | Citations | PageRank |
3-540-33170-0 | 0 | 0.34 |
References | Authors | |
1 | 1 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| John Rushby | 1 | 2459 | 235.69 |