AbstractAction Systems is a predicate transformer based formalism. It supports the development of provably correct reactive and distributed systems by refinement. Recently, Action Systems were extended with a differential action. It is used for modelling continuous behaviour, thus, allowing the use of refinement in the development of provably correct hybrid systems, i.e., a discrete controller interacting with some continuously evolving environment. However, refinement as a method is concerned with correctness issues only. It offers very little guidance in what details one should consider during the refinement steps to make the system more robust. That information is revealed by robustness analysis. Other formalisms not supporting refinement do have tool support for automating the robustness analysis, e.g., HyTech for linear hybrid automata. Consequently, we study in this paper the non-trivial translation problem between Action Systems and linear hybrid automata. As the main contribution, we give and prove correct an algorithm that translates a linear hybrid action system to a linear hybrid automaton. With this algorithm we combine the strengths of the two formalisms: we may use HyTech for the robustness analysis to guide the development by refinement.
Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification; F.1.1 [Computation by Abstract Devices]: Models of Computation; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; J.7 [Computers in Other Systems]
Additional Key Words and Phrases: action systems, linear hybrid systems, transition systems, linear hybrid automata
Selected references
- R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In Proceedings of the Second Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pages 131-142, Montreal, Quebec, Canada, 17-19 August 1983.
- Thomas A. Henzinger. The theory of hybrid automata. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 278-292, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.