Foundations of Cyber-Physical Systems (CPS)

Cyber-Physical Systems (CPS) are integrations of computation and physical processes. Embedded computers and networks monitor and control the physical processes, with feedback loops where physical processes affect computations and vice versa. The economic and societal potential of such systems is vastly greater than what has been realized, and major investments are being made worldwide to develop the technology. The technology builds on the older (but still very young) discipline of embedded systems, computers and software embedded in devices whose principle mission is not computation, such as cars, toys, medical devices, and scientifi c instruments. CPS integrates the dynamics of the physical processes with those of the software and networking, providing abstractions and modeling, design, and analysis techniques for the integrated whole.

As a discipline, CPS is an engineering discipline, focused on technology, with a strong foundation in mathematical abstractions. It shares many of these abstractions with computer science, but requires adapting them to embrace the dynamics of the physical world. Computer science, as rooted in the Turing-Church notion of computability, abstracts away core physical properties, such as the passage of time, that are required to include the dynamics of the physical world in the domain of discourse.

CHESS is pursuing foundational research in the abstractions and analytical techniques of CPS. Two such efforts are described here.

Timed Discrete-Event Systems

In the context of timed discrete-event systems, processes are allowed to realize functions that are not order-preserving with respect to the prefix ordering relation on the communicated sequences of values. This property renders naive applications of traditional domain-theoretic models inadequate for the semantic interpretation of such systems. Yet, interesting results have been obtained by imposing a fixed lower bound on the reaction time of the involved processes, effectively precluding Zeno behavior.

This work focuses on relaxing this requirement to obtain semantic interpretations even in the presence of Zeno conditions. The underlying aim is to establish a canonical denotational definition of timed discrete-event programming languages, thereby providing the means for reasoning about the correctness of the individual implementations, as well as allowing hidden commonalities of seemingly different timed systems to emerge.

Compositional Dataflow

Dataflow is a model of computation where a collection of actors communicate through unidirectional first-in first-out (FIFO) channels. Each dataflow actor is defined as a set of firing rules and a firing function. Firing rules specify what tokens must be available at the inputs for the actor to fire. The firing function specifies the input tokens consumed and the output tokens produced when the actor fires, and possibly a new set of firing rules along with a new firing function, thus reflecting an update to the state of the actor. Under suitable conditions, these actors define continuous functions, typically referred to as dataflow processes, over the complete partial order (CPO) of all finite and infinite sequences of tokens under the natural prefix order, and therefore provide for an alternative implementation of Kahn process networks.

Despite the abundance of dataflow applications in the embedded systems community, dataflow does not qualify as a programming language. Unless an evaluation strategy is specified, it is impossible to provide a semantic interpretation that will unambiguously assign a meaning to a dataflow network. A considerable amount of research has centered around evaluation strategies that will adhere to Kahn's least fixed-point solution. However, tailoring the operational semantics of a language to fit the simplicity and mathematical convenience of a particular denotational semantics is somewhat questionable. Park's bounded scheduling policy stands out for promoting bounded execution at the expense of convergence to Kahn's least fixed-point semantics. Nonetheless, it compromises compositionality and renders dataflow programming and execution intractable to formal reasoning.

This work focuses on a formal operational semantics for a dataflow programming language. The objective is to identify a set of computation rules that can yield bounded execution whenever possible, and at the same time remain uncoupled from the low-level machine details, and hence be more amenable to formal analysis. The notion of compositionality serves as a compass in this process, offering a solid correctness criterion for the proposed formalism. Questions on optimality issues are also to be addressed.

CHESS graduate students Yasemin Demir, Jeff Jensen, and Eleftherios Matsikoudis.

Cyber-Physical Systems News

May 12, 2009: The U.S. House of Representatives passed H.R. 2020, the Networking and Information Technology Research and Development Act of 2009:
"Additionally, it creates a task force to explore mechanisms for carrying out collaborative R&D activities in cyber-physical systems;"
April 13-16, 2009: CPS Week held in San Francisco
July 31, 2008: Don Winter (Boeing) and others testify in front of the House Science and technology committee about Cyber-Physical Systems (CPS) and other topics.
April 21, 2008: Workshop: From Embedded Systems to Cyber-Physical Systems: a Review of the State-of-the-Art and Research Needs, St. Louis, MO.

CPS Publications.

Mailing lists and discussion forums may be found under the cps link above.

To modify this page, use CVS.

You are not logged in