Architecture-Centric Modeling, Analysis, and Verification of Cyber-Physical Systems

NII Shonan Meeting:

@ Shonan Village Center, March 21-24, 2016

NII Shonan Meeting Report (ISSN 2186-7437):No.2016-5

Organizers

  • Shin Nakajima, NII, Japan
  • Jean-Pierre Talpin, INRIA, France
  • Masumi Toyoshima, Denso Corporation, Japan
  • Huafeng Yu, Toyota InfoTechnology Center, USA

Overview

073_Group Photo Description of the meeting

1.1 Context
The term cyber-physical system (CPS) was introduced by Helen Gill at the NSF referring to the integration of computation and physical processes. In CPS, embedded computers and networks monitor and control the physical processes, usually with feedback loops where physical processes affect computations and vice versa. The principal challenges in system design lie in this perpetual interaction of software, hardware and physics.

CPS safety is often critical for society in many applications such as transportations (whether automotive, trains or airplanes), power distribution, medical equipment and tele-medicine. Whether or not life is threatened, failures may have huge economic impact. The development of reliable CPS has become a critical issue for the industry and society. Safety and security requirements must be satisfied by using strong validation tools. Requirements for quality of service, safety and security imply to have formally proved the required properties of the system before it is deployed.
In the past 15 years, development has moved towards Model Driven Engineering (MDE).  With MDE methodology,  requirements are gathered with use cases, then a model of the system is built that satisfy the requirements. Several modelling formalisms have appeared in the past ten years.
The most successful are the executable models, models that can be exercised, tested and validated. This approach can be used for both software and hardware.

A common feature of CPS is the predominance of concurrency and parallelism in models. Development of concurrent and parallel systems has traditionally been clearly split in two different families. The first family is based on synchronous models, primarily targeting design of hardware circuits and/or embedded and reactive systems, often safety-critical. Esterel, Lustre, Signal and SCADE are examples of existing technologies of that nature, and in many places these have been connected with models of environments as required for CPS modelling. The second family addresses more loosely coupled systems, where communication between distributed entities is asynchronous by nature. Large systems are increasingly mixing both types of concurrency: they are structured hierarchically and comprise multiple synchronous devices connected by buses or networks that
communicate asynchronously.

In an architectural model, a CPS is represented by a distributed system as entities with well-defined interfaces, connections between ports on component interfaces, and specifies component properties that can be used in analytical reasoning about the model. Models are hierarchically organized: each component can contain another sub-system with its own set of components and connections between them. An architecture description language for embedded systems, for which timing and resource availability form an important part of requirements, must in addition describe resources of the system platform, such as processors, memories, communication links, etc. Several architectural modelling languages for embedded systems have emerged in recent years, including the SAE AADL1, SysML2, UML MARTE3.

An architectural specification serves several important purposes. First, it breaks down a system model into manageable components to establish clear interfaces between components. In this way, complexity becomes manageable by hiding details that are not relevant at a given level of abstraction. Clear, formally defined, component interfaces allow us to avoid integration problems 1Architecture Analysis and Design Language, AS-5506. SAE, 2004. http://standards.sae.org/as5506b 2System Modelling Language. OMG, 2007. http://www.omg.org/spec/SysML at the implementation phase. Connections between components, which specify how components affect each other, help propagate the effects of a change in one component to the linked components.
More importantly, an architectural model is a repository to share knowledge about the system being designed. This knowledge can be represented as requirements, design artefacts, component implementations, held together by a structural backbone. Such a repository enables automatic generation of analytical models for different aspects of the system, such as timing, reliability,
security, performance, energy, etc.

Since all the models are generated from the same source, the consistency of assumptions w.r.t. guarantees, of abstractions w.r.t. refinements, used for different analyses becomes easier, and can be properly ensured in a design methodology based on formal verification and synthesis methods, using notions such as formally defined interfaces and contracts.

In most cases, however, quantitative reasoning in architecture modelling and CPS is predominantly parameterised by the dimension of time. In each of the viewpoints that an architecture or CPS model refers to: software, hardware, physic, time takes a different form: continuous or discrete, event-based or time-triggered. It is therefore of prime importance to mitigate heteroge-
neous notions of time to support quantitative reasoning in system design, either using a tentatively unified model for it, or by formalizing abstraction/refinement relations from one to another in order to mitigate heterogeneity.

1.2 Purpose of the seminar
The proposed seminar will bring together researchers who are interested in defining precise semantics of an architecture description language, using it for building tools that generate analytical models, for the purpose of simulation and formal verification (simulation, components integration, requirements validation) code generation (interfaces, orchestration, scheduling).

Despite recent research activity in this area, to formally define or semantically interpret architectural models, we observe a significant gap between the state of the art and practical needs to handle evolvingly complex models. In practice, most approaches cover a limited subset of the language and target a small number of modelling patterns. A more general approach would most likely require semantic interpretation (an abstraction, a refinement) of the source architecture model by
the target analytic tool, instead of hard-coding semantics and patterns into the model generator.

  • How to support modelling in the large, in different dimensions? The architectural description
    should tie together system requirements, platform requirements, highlight tradeooffs, etc. How to formalize these requirements and to assess them with respect to real-time?
  • How to provide a better description of the semantics for an architecture description language in a way that is both easier to understand by humans and easier to interpret by a tool? Thus user-friendly semantics should be soundly linked with existing verification tools. We also envision to enhance the model with the certification credits provided by the validation.
  • How to handle extension of the semantics to address new demanding architectures like multi-core, new network technologies, and their application to large-scale systems?
  • How to model complex architectural frameworks, such as synchronous or time-triggered designs, RAVENSCAR-compliant systems, _ How to interconnect the architecture modelling of software-intensive embedded systems to physical concerns like energy consumption, electro-magnetic compatibility?
  • How to provide sound, cross-domains, timed/quantitative reasoning in system design to integrate inherently heterogeneous component models ?

To address these issues, and foster the exchange of novel ideas, approaches, frameworks to tackle the above fundamental issues, we will invite internationally acknowledged experts in each of every viewpoint of the problem at hand, and means to put them through. Various collaborations are likely to be fostered, e.g. common handbook or point-to-point collaborations being setup.