On implementing real-time specification patterns using observers

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

doi:10.1007/978-3-319-40648-0_2

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 proceeding › Conference contribution

4 Scopus citations

Abstract

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 language	English (US)
Title of host publication	NASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings
Editors	Oksana Tkachuk, Sanjai Rayadurgam
Publisher	Springer- Verlag
Pages	19-33
Number of pages	15
ISBN (Print)	9783319406473
DOIs	https://doi.org/10.1007/978-3-319-40648-0_2
State	Published - Jan 1 2016
Event	8th International Symposium on NASA Formal Methods, NFM 2016 - Minneapolis, United States Duration: Jun 7 2016 → Jun 9 2016

Publication series

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

Conference

Conference	8th International Symposium on NASA Formal Methods, NFM 2016
Country/Territory	United States
City	Minneapolis
Period	6/7/16 → 6/9/16

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.

Access

10.1007/978-3-319-40648-0_2

OpenUrl availability

Full text

Cite this

Backes, J. D., Whalen, M. W., Gacek, A., & Komp, J. (2016). On implementing real-time specification patterns using observers. In O. Tkachuk, & S. Rayadurgam (Eds.), NASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings (pp. 19-33). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9690). Springer- Verlag. https://doi.org/10.1007/978-3-319-40648-0_2

On implementing real-time specification patterns using observers. / Backes, John D.; Whalen, Michael W.; Gacek, Andrew et al.
NASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings. ed. / Oksana Tkachuk; Sanjai Rayadurgam. Springer- Verlag, 2016. p. 19-33 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9690).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Backes, JD, Whalen, MW, Gacek, A & Komp, J 2016, On implementing real-time specification patterns using observers. in O Tkachuk & S Rayadurgam (eds), NASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9690, Springer- Verlag, pp. 19-33, 8th International Symposium on NASA Formal Methods, NFM 2016, Minneapolis, United States, 6/7/16. https://doi.org/10.1007/978-3-319-40648-0_2

Backes JD, Whalen MW, Gacek A, Komp J. On implementing real-time specification patterns using observers. In Tkachuk O, Rayadurgam S, editors, NASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings. Springer- Verlag. 2016. p. 19-33. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-40648-0_2

Backes, John D. ; Whalen, Michael W. ; Gacek, Andrew et al. / On implementing real-time specification patterns using observers. NASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings. editor / Oksana Tkachuk ; Sanjai Rayadurgam. Springer- Verlag, 2016. pp. 19-33 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{11e0b61c863b46e280440079a8ee6511,

title = "On implementing real-time specification patterns using observers",

abstract = "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.",

author = "Backes, {John D.} and Whalen, {Michael W.} and Andrew Gacek and John Komp",

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: {\textcopyright} Springer International Publishing Switzerland 2016.; 8th International Symposium on NASA Formal Methods, NFM 2016 ; Conference date: 07-06-2016 Through 09-06-2016",

year = "2016",

month = jan,

day = "1",

doi = "10.1007/978-3-319-40648-0_2",

language = "English (US)",

isbn = "9783319406473",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer- Verlag",

pages = "19--33",

editor = "Oksana Tkachuk and Sanjai Rayadurgam",

booktitle = "NASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings",

}

TY - GEN

T1 - On implementing real-time specification patterns using observers

AU - Backes, John D.

AU - Whalen, Michael W.

AU - Gacek, Andrew

AU - Komp, John

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

PY - 2016/1/1

Y1 - 2016/1/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=84976614139&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84976614139&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-40648-0_2

DO - 10.1007/978-3-319-40648-0_2

M3 - Conference contribution

AN - SCOPUS:84976614139

SN - 9783319406473

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 19

EP - 33

BT - NASA Formal Methods - 8th International Symposium, NFM 2016, Proceedings

A2 - Tkachuk, Oksana

A2 - Rayadurgam, Sanjai

PB - Springer- Verlag

T2 - 8th International Symposium on NASA Formal Methods, NFM 2016

Y2 - 7 June 2016 through 9 June 2016

ER -

On implementing real-time specification patterns using observers

Abstract

Publication series

Conference

Bibliographical note

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this