On implementing real-time specification patterns using observers

John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations


English language requirements are often used to specify the behavior of complex cyber-physical systems. The process of transforming these requirements to a formal specification language is often challenging, especially if the specification language does not contain constructs analogous to those used in the original requirements. For example, requirements often contain real-time constraints, but many specification languages for model checkers have discrete time semantics. Work in specification patterns helps to bridge these gaps, allowing straightforward expression of common requirements patterns in formal languages. In this work we demonstrate how we support real-time specification patterns in the Assume Guarantee Reasoning Environment (AGREE) using observers. We demonstrate that there are subtle challenges, not mentioned in previous literature, to express real-time patterns accurately using observers. We then demonstrate that these patterns are sufficient to model real-time requirements for a real-world avionics system.

Original languageEnglish (US)
Title of host publicationNASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings
EditorsOksana Tkachuk, Sanjai Rayadurgam
PublisherSpringer- Verlag
Number of pages15
ISBN (Print)9783319406473
StatePublished - Jan 1 2016
Event8th International Symposium on NASA Formal Methods, NFM 2016 - Minneapolis, United States
Duration: Jun 7 2016Jun 9 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference8th International Symposium on NASA Formal Methods, NFM 2016
Country/TerritoryUnited States

Bibliographical note

Funding Information:
This work was sponsored by DARPA/AFRL Contract FA8750-12-9-0179, AFRL Contract FA8750-16-C-0018, and NASA Contract NNA13AA21C.

Publisher Copyright:
© Springer International Publishing Switzerland 2016.


Dive into the research topics of 'On implementing real-time specification patterns using observers'. Together they form a unique fingerprint.

Cite this