10. – 15. Februar 2019, Dagstuhl-Seminar 19071

Specification Formalisms for Modern Cyber-Physical Systems


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

Auskunft zu diesem Dagstuhl-Seminar erteilen

Jutka Gasiorowski zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen


Gemeinsame Dokumente


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:

  1. 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?
  2. 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?
  3. 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.
  4. 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


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


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


Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.