February 10 – 15 , 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)

For support, please contact

Dagstuhl Service Team


List of Participants
Shared Documents

Press Room


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


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).


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