Dagstuhl Seminar 19071
Specification Formalisms for Modern Cyber-Physical Systems
( Feb 10 – Feb 15, 2019 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/19071
Organizers
- Jyotirmoy Deshmukh (USC - Los Angeles, US)
- Oded Maler (VERIMAG - Grenoble, FR)
- Dejan Nickovic (AIT - Austrian Institute of Technology - Wien, AT)
Contact
- Michael Gerke (for scientific matters)
- Jutka Gasiorowski (for administrative matters)
Specification plays a central role in evaluating system behaviors. The development of modern cyber-physical systems (CPS) requires reasoning about safety, performance, security, privacy, and reliability aspects. We can observe that today there is no specification language that allows describing such heterogeneous CPS requirements. This Dagstuhl Seminar proposes to bring together researchers and practitioners from diverse fields related to CPS, such as the automotive, avionics, medical devices, healthcare, robotics, financial applications, smart energy and manufacturing systems in a quest for developing a new, comprehensive and as unified as possible specification formalism for modern CPS. The short-term objective of the Dagstuhl seminar is to identify challenges in formally specifying the desired observable behaviors of systems that combine continuous-time evolution and discrete events, as is the typical case for CPS. In addition to specifications related to functional safety of CPS systems, we wish to identify challenges in specifying performance, security, privacy and information-flow properties for CPS systems. This Dagstuhl seminar will also explore the intersection of machine learning and formal specification languages. In particular, formal specifications can also serve as a bridge between the world of verification and the world of learning and data-mining that attempts to solve the inverse problem of finding a concise description of observable behaviors.
The longer-term objective is to propose a standard specification language for CPS applications, in a similar vein as specification languages for digital hardware designs. Realizing such an objective may require forming a standards committee, and convincing tool-makers for industrial CPS designs to adopt such a standard specification language.
We identify the following main challenges that we would need to address in designing such a specification language:
- Expressiveness: What are the real needs of a CPS engineer? Do we need to check, measure or learn a property? How do we tackle and integrate specific (and sometimes conflicting) requirements aspects (time, frequency, security, privacy, data integrity, etc.) in a specification language?
- Monitorability: What are the specifications that we can monitor in real-time? How do we pass from monitoring a CPS at design time to monitoring a CPS at deployment time? How do we tackle sensor inaccuracies and partial observability?
- Relation to other ways to evaluate behaviors: In contrast with logical formalisms that essentially look for extremal behaviors in data, many standard evaluation tools used in engineering disciplines compute statistical metrics such as average, variance/covariance, etc. on the observed data. Further, data could be noisy, which may require reasoning techniques from machine learning and statistics.
- Ease of Use: Is an average CPS engineer going to adopt a specification formalism based on logic? How do we make the specification language more accessible (visual specifications, libraries of reusable templates, etc.)? How do we effectively teach a specification language to a new user?
This Dagstuhl seminar will have a confluence of diverse researchers from academia and industry and will provide a unique opportunity to start a concerted effort on making specification language standards for cyber-physical systems.
Creative Commons BY 3.0 DE
Jyotirmoy Deshmukh, Oded Maler, and Dejan Nickovic
Press Reviews
- Castles - Modern Science in Old Walls
TV report by Emil Mura, first aired in SR TV on May 2, 2019
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.
The 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:
- Identification of various benchmark problems for monitoring specifications at runtime, and learning specifications from data.
- Standardizing syntax for expressing time-series data, such as comma separated values (CSV) with a well-defined header file.
- Creating a public repository containing traces, specifications, models, and pattern libraries.
- 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.
- 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
- Specification languages in digital hardware
- Tools perspective
- Overview of declarative specification languages
Days 2 and 3 Domain-specific needs and domain-specific specification formalisms
- Specifications in automotive systems
- Specifications in robotics and perception
- Specifications in Industry 4.0, EDA and mixed signal design
- Specifications in smart cities
- Specifications in bioloty
- Specifications in medical devices
- Specifications in security
Days 4 Expressivity, monitoring algorithms and analysis concerns
- Algorithms for specifications: specifications for learning versus learning specifications
- Streaming languages
- Runtime monitoring
- 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.
Jyotirmoy Deshmukh and Dejan Nickovic
- Houssam Abbas (Oregon State University - Corvallis, US) [dblp]
- Nikos Aréchiga (Toyota Research Institute - Los Altos, US) [dblp]
- Ezio Bartocci (TU Wien, AT) [dblp]
- Marcello M. Bersani (Polytechnic University of Milan, IT) [dblp]
- Paul Bogdan (USC - Los Angeles, US) [dblp]
- Borzoo Bonakdarpour (Iowa State University - Ames, US) [dblp]
- Chih-Hong Cheng (fortiss GmbH - München, DE) [dblp]
- Thao Dang (VERIMAG - Grenoble, FR) [dblp]
- Jyotirmoy Deshmukh (USC - Los Angeles, US) [dblp]
- Rayna Dimitrova (University of Leicester, GB) [dblp]
- Alexandre Donzé (Decyphir - Moirans, FR) [dblp]
- Katie Driggs-Campbell (University of Illinois - Urbana Champaign, US) [dblp]
- Georgios Fainekos (Arizona State University - Tempe, US) [dblp]
- Lu Feng (University of Virginia - Charlottesville, US) [dblp]
- Thomas Ferrère (IST Austria - Klosterneuburg, AT) [dblp]
- Bernd Finkbeiner (Universität des Saarlandes, DE) [dblp]
- Dana Fisman (Ben Gurion University - Beer Sheva, IL) [dblp]
- Felipe Gorostiaga (IMDEA Software - Madrid, ES) [dblp]
- Radu Grosu (TU Wien, AT) [dblp]
- James Kapinski (Toyota Research Institute North America- Ann Arbor, US) [dblp]
- Martin Leucker (Universität Lübeck, DE) [dblp]
- Rupak Majumdar (MPI-SWS - Kaiserslautern, DE) [dblp]
- Niveditha Manjunath (AIT - Austrian Institute of Technology - Wien, AT) [dblp]
- Stefan Mitsch (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Laura Nenzi (University of Trieste, IT) [dblp]
- Dejan Nickovic (AIT - Austrian Institute of Technology - Wien, AT) [dblp]
- Jens Oehlerking (Robert Bosch GmbH - Stuttgart, DE) [dblp]
- Ana Oliveira da Costa (TU Wien, AT) [dblp]
- Necmiye Ozay (University of Michigan - Ann Arbor, US) [dblp]
- Pavithra Prabhakar (Kansas State University - Manhattan, US) [dblp]
- Gustavo Quirós (Siemens - Princeton, US) [dblp]
- Akshay Rajhans (MathWorks, US) [dblp]
- David Safranek (Masaryk University - Brno, CZ) [dblp]
- César Sánchez (IMDEA Software - Madrid, ES) [dblp]
- Caleb Stanford (University of Pennsylvania - Philadelphia, US) [dblp]
- Hazem Torfah (Universität des Saarlandes, DE) [dblp]
- Marcell Vazquez-Chanlatte (University of California - Berkeley, US) [dblp]
Classification
- artificial intelligence / robotics
- semantics / formal methods
- verification / logic
Keywords
- specifications
- requirements
- monitoring
- verification
- cyber-physical systems
