2018/03/08 by Andre Metelo, Metelo, Andre, Christiano Braga +3
Computer Science · #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques
paper · pdf · doi:10.48550/arxiv.1803.03173
openalex publication_date 2018/03/08 · openalex created_date 2022/10/06 · openalex updated_date 2026/07/28
Cyber-Physical Systems (CPS) are systems controlled by one or more\ncomputer-based components tightly integrated with a set of physical components,\ntypically described as sensors and actuators, that can either be directly\nattached to the computer components, or at a remote location, and accessible\nthrough a network connection. The modeling and verification of such systems is\na hard task and error prone that require rigorous techniques. Hybrid automata\nis a formalism that extends finite-state automata with continuous behavior,\ndescribed by ordinary differential equations. This paper uses a rewriting\nlogic-based technique to model and validate CPS, thus exploring the use of a\nformal technique to develop such systems that combines expressive specification\nwith efficient state-based analysis. Moreover, we aim at the modular\nspecification of such systems such that each CPS component is independently\nspecified and the final system emerges as the synchronous product of its\nconstituent components. We model CPSs using Linear Hybrid Automaton and\nimplement them in Real-Time Maude, a rewriting logic tool for real-time\nsystems. With this method, we develop a specification for the n-reservoir\nproblem, a CPS that controls a hose to fill a number of reservoirs according to\nthe physical properties of the hose and the reservoirs.\n