https://www.dagstuhl.de/19071

February 10 – 15 , 2019, Dagstuhl Seminar 19071

Specification Formalisms for Modern Cyber-Physical Systems

Organizers

Jyotirmoy Deshmukh (USC – Los Angeles, US)
Oded Maler (VERIMAG – Grenoble, FR)
Dejan Nickovic (AIT – Austrian Institute of Technology – Wien, AT)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 9, Issue 2 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents

Summary

Modern Cyber-Physical Systems (CPS) represent the convergence of the fields of control theory, artificial intelligence, machine learning, and distributed communication/coordination. CPS applications range from small quad-rotor based aerial vehicles to commercial airplanes, from driverless autonomous vehicles to vehicle platoons, from nano-scale medical devices in closed-loop with a human to giga-scale industrial manufacturing systems. While several application domains can claim to be cyber-physical systems, a unique aspect of CPS is a strong focus on model-based development (MBD). The MBD paradigm allows analyzing the system virtually, examining its safety, performance, stability, security, privacy, or resilience. At a certain level of abstraction, a model of a CPS application can be roughly divided into three parts: (1) the plant model representing an encapsulation of the physical components in the system, (2) the controller model representing the software used to regulate the plant, and (3) an environment model representing exogenous disturbances to the plant.

Given plant, controller and environment models of a system, in order to perform any of the aforementioned analyses, a crucial step is to articulate the goal of the analysis as a formal specification for the system. The analysis problem can then check whether the system implementation is a refinement of its specification. However, the state-of-the-art in industrial settings is that formal specifications are rarely found. Specifications exist in the form of mental models of correctness formed by engineers through their design insights and experience, or visual depictions in the form of simulation plots, and occasionally as legacy scripts and monitors. None of these are formal, machine-checkable unambiguous specifications. In the industry, engineers often use the term requirements instead of specifications. Typical industrial requirements do not arise from principled software engineering approaches to develop CPS software, but rather are summaries of discussions between developers and their customers. While the state-of-the-art for requirements/specifications in industrial settings is far from ideal, in academic settings, there is a problem of having a wide choice between a number of specification formalisms, primarily being developed by the formal methods community. On the other hand, application-specific academic domains such as robotics, biological systems, and medical devices may not always articulate formal system specifications.

he overarching goal of the seminar was thus to address the following question: Is there a universal specification formalism that can be used as a standard language for a variety of modern cyber-physical systems? To address this question, this seminar was divided into three broad thrusts:

  • State-of-the-art in general specification formalisms,
  • Domain-specific needs and domain-specific specification formalisms,
  • Expressivity, Monitoring Algorithms and Analysis concerns for a specification language.

Outcome of the Seminar

The seminar had a total of $37$ participants with a mix of research communities including experts (both theoreticians and practitioners) in formal methods, runtime monitoring, machine learning, control theorey, industrial IoT, and biological systems. The seminar focused on the cross-domain challenges in the development of a universal specification formalism that can accommodate for various CPS applications.

The seminar provided an excellent overview of requirements from various application domains that paved the road for identifying common features in a cross-domain specification language. As another outcome of the seminar, we defined as a community the following next steps:

  1. Identification of various benchmark problems for monitoring specifications at runtime, and learning specifications from data.
  2. Standardizing syntax for expressing time-series data, such as comma separated values (CSV) with a well-defined header file.
  3. Creating a public repository containing traces, specifications, models, and pattern libraries.
  4. Coordination with RVComp, a runtime verification competition collocated with the Runtime Verification (RV) conference, and possible coordination with SygusComp (Syntax-guided synthesis competition) and SYNTComp (Synthesis competition) to arrange special tracks on learning specifications.
  5. Creating a public repository containing standard parsers for variety of specification formalisms such as variants of Signal Temporal Logic.

Sessions

The seminar was organized as a sequence of open discussions on pre-defined topics of interest. Each session had one or two moderators who introduced the topic and one or two scribes who recorded the proceedings of the discussions. The moderators had a short introduction of the topic, identifying the most important sub-topics for open discussion. The discussions were structured in following sessions:

Day 1 State-of-the-art in general specification formalisms

  1. Specification languages in digital hardware
  2. Tools perspective
  3. Overview of declarative specification languages

Days 2 and 3 Domain-specific needs and domain-specific specification formalisms

  1. Specifications in automotive systems
  2. Specifications in robotics and perception
  3. Specifications in Industry 4.0, EDA and mixed signal design
  4. Specifications in smart cities
  5. Specifications in bioloty
  6. Specifications in medical devices
  7. Specifications in security

Days 4 Expressivity, monitoring algorithms and analysis concerns

  1. Algorithms for specifications: specifications for learning versus learning specifications
  2. Streaming languages
  3. Runtime monitoring
  4. Expressivity

Day 5 Next steps and summary of the seminar outcomes

We also organized on Day 1 a session to honor the memory of Oded Maler, one of the co-organizers of this seminar, and who sadly passed away in September 2018.

Summary text license
  Creative Commons BY 3.0 Unported license
  Jyotirmoy Deshmukh and Dejan Nickovic

Classification

  • Artificial Intelligence / Robotics
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Specifications
  • Requirements
  • Monitoring
  • Verification
  • Cyber-physical systems

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

NSF young researcher support