NDLI: A framework for high-assurance quasi-synchronous systems

Content Provider	IEEE Xplore Digital Library
Author	Larrieu, R. Shankar, N.
Copyright Year	2014
Description	Author affiliation: Ecole Polytech., Palaiseau, France (Larrieu, R.) \|\| SRI Int., Menlo Park, CA, USA (Shankar, N.)
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).
Starting Page	72
Ending Page	83
File Size	636809
Page Count	12
File Format	PDF
ISBN	9781479953387
DOI	10.1109/MEMCOD.2014.6961845
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2014-10-19
Publisher Place	Switzerland
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Computational modeling Synchronization Delays Computer architecture Sensors Actuators Robots
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A framework for high-assurance quasi-synchronous systems

A Dynamics Simulation Architecture for Robotic Systems

Communication framework for sensor-actuator data in mobile robots

A novel modeling framework for time-triggered safety-critical embedded systems

High Assurance Smart Grid: Smart Grid Control Systems Communications Architecture

A behavior-based control architecture

Automatic construction of diagnoser for complex discrete event systems

Object oriented design of a mobile robot using UML

Co-simulation of embedded systems in a heterogeneous MoC-based modeling framework

A framework for high-assurance quasi-synchronous systems

Similar Documents

A framework for high-assurance quasi-synchronous systems

A Dynamics Simulation Architecture for Robotic Systems

Communication framework for sensor-actuator data in mobile robots

A novel modeling framework for time-triggered safety-critical embedded systems

High Assurance Smart Grid: Smart Grid Control Systems Communications Architecture

A behavior-based control architecture

Automatic construction of diagnoser for complex discrete event systems

Object oriented design of a mobile robot using UML

Co-simulation of embedded systems in a heterogeneous MoC-based modeling framework

A framework for high-assurance quasi-synchronous systems