DocumentCode :
159097
Title :
A framework for high-assurance quasi-synchronous systems
Author :
Larrieu, Robin ; Shankar, Nishanth
Author_Institution :
Ecole Polytech., Palaiseau, France
fYear :
2014
fDate :
19-21 Oct. 2014
Firstpage :
72
Lastpage :
83
Abstract :
The design of a complex cyber-physical system is centered around one or more models of computation (MoCs). These models define the semantic framework within which a network of sensors, controllers, and actuators operate and interact with each other. In this paper, we examine the foundations of a quasi-synchronous model of computation Our version of the quasi-synchronous model is inspired by the Robot Operating System (ROS). It consists of nodes that encapsulate computation and topic channels that are used for communicating between nodes. The nodes execute with a fixed period with possible jitter due to local clock drift and scheduling uncertainties, but are not otherwise synchronized. The channels are implemented through a mailbox semantics. In each execution step, a node reads its incoming mailboxes, applies a next-step operation to update its local state, and writes to all its outgoing mailboxes. The underlying transport mechanism implements the mailbox-to-mailbox data transfer with some bounded latency. Messages can be lost if a mailbox is over-written before it is read. We prove a number of basic theorems that are useful for designing robust high-assurance cyber-physical systems using this simple model of computation. We show that depending on the relative rates of the sender and receiver, there is a bound on the number of consecutive messages that can be lost. By increasing the mailbox queue size to a given bound, message loss can be eliminated. We demonstrate that there is a bound on the age of inputs that are used in any processing step. This in turn can be used to bound the end-to-end sense-control-actuate latency. We illustrate how these theorems are useful in designing and verifying a thermostat-based heating system. Our proofs have been mechanically verified using the Prototype Verification System (PVS).
Keywords :
control engineering computing; program verification; robust control; thermal variables control; thermostats; MoC; PVS; ROS; bounded latency; complex cyber-physical system; consecutive messages; end-to-end sense-control-actuate latency; high-assurance quasisynchronous systems; jitter; local clock drift; mailbox queue size; mailbox semantics; mailbox-to-mailbox data transfer; models of computation; prototype verification system; robot operating system; robust high-assurance cyber-physical systems; scheduling uncertainties; thermostat-based heating system; topic channels; Actuators; Computational modeling; Computer architecture; Delays; Robots; Sensors; Synchronization;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Formal Methods and Models for Codesign (MEMOCODE), 2014 Twelfth ACM/IEEE International Conference on
Conference_Location :
Lausanne
Type :
conf
DOI :
10.1109/MEMCOD.2014.6961845
Filename :
6961845
Link To Document :
بازگشت