Semi-automatic controller design of Java-like models
2013
Controller synthesis consists in automatically generating a controller to restrict a hardware or software system so that it respects given requirements, for instance safety properties. Existing synthesis tools for discrete event systems mainly solve the problem for systems described in low-level formalisms. Controller synthesis, however, is not used in most industrial engineering processes. Barriers to wider adoption are the complexity of formally expressing the system and its requirements, the state explosion induced by large systems, and the limited confidence in the result, due to the difficulty in understanding the generated code. We propose an iterative, incremental, and semi-automatic approach to controller design, supporting the engineering process and mitigating state space explosion during synthesis. To provide a high-level environment, our approach is implemented in VeriJ, a Java-like language, and illustrated on a significant example taken from automated transport systems.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
18
References
0
Citations
NaN
KQI