Skip to main content
SpringerLink
Log in

On Implementing Real-Time Specification Patterns Using Observers

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9690))

Included in the following conference series:

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.

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

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Although our formalisms are expressed as Lustre specifications, the concepts and proofs presented in this paper are applicable to many other popular model checking specification languages.

  2. 2.

    AGREE is available at: http://loonwerks.com.

  3. 3.

    In practice, we allow a timeout to be a negative number to represent infinity. This maintains the correct semantics for the constraint for t in Formula 1.

  4. 4.

    The single pattern that cannot be implemented requires an independent event to occur for each of an unbounded number of causes. There are 12 functional and timing RSL patterns in total.

References

  1. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411–420. IEEE (1999)

    Google Scholar 

  2. Konrad, S., Cheng, B.H.: Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering, pp. 372–381. ACM (2005)

    Google Scholar 

  3. Gruhn, V., Laue, R.: Patterns for timed property specifications. Electron. Notes Theoret. Comput. Sci. 153, 117–133 (2006)

    Article  Google Scholar 

  4. Bellini, P., Nesi, P., Rogai, D.: Expressing and organizing real-time specification patterns via temporal logics. J. Syst. Softw. 82, 183–196 (2009)

    Article  Google Scholar 

  5. Reinkemeier, P., Stierand, I., Rehkop, P., Henkler, S.: A pattern-based requirement specification language: mapping automotive specific timing requirements. In: Fachtagung des GI-Fachbereichs Softwaretechnik, pp. 99–108 (2011)

    Google Scholar 

  6. Etzien, C., Gezgin, T., Froschle, S., Henkler, S., Rettberg, A.: Contracts for evolving systems. In: ISORC, pp. 1–8 (2013)

    Google Scholar 

  7. Alur, R.: Techniques for automatic verification of real-time systems. Ph.D. thesis, stanford university (1991)

    Google Scholar 

  8. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-time Syst. 2, 255–299 (1990)

    Article  Google Scholar 

  9. Moser, L.E., Ramakrishna, Y., Kutty, G., Melliar-Smith, P.M., Dillon, L.K.: A graphical environment for the design of concurrent real-time systems. ACM Trans. Softw. Eng. Methodol. (TOSEM) 6, 31–79 (1997)

    Article  Google Scholar 

  10. Abid, N., Dal Zilio, S., Le Botlan, D.: Real-time specification patterns and tools. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 1–15. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  11. Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language LUSTRE. Proc. IEEE 79, 1305–1320 (1991)

    Article  Google Scholar 

  12. Backes, J., Cofer, D., Miller, S., Whalen, M.W.: Requirements analysis of a quad-redundant flight control system. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 82–96. Springer, Heidelberg (2015)

    Google Scholar 

  13. Murugesan, A., Heimdahl, M.P., Whalen, M.W., Rayadurgam, S., Komp, J., Duan, L., Kim, B.G., Sokolsky, O., Lee, I.: From requirements to code: model based development of a medical cyber physical system. SEHC (2014)

    Google Scholar 

  14. Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126–140. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  15. Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language, 1st edn. Addison-Wesley Professional, Reading (2012)

    Google Scholar 

  16. CESAR: The CESAR project (2010). http://www.cesarproject.eu/

  17. Dutertre, B., Sorea, M.: Timed systems in SAL. Technical report, SRI International (2004)

    Google Scholar 

  18. Pike, L.: Real-time system verification by \(k\)-induction. Technical report, NASA (2005)

    Google Scholar 

  19. Gao, J., Whalen, M., Van Wyk, E.: Extending lustre with timeout automata. In: SLA++P (2007)

    Google Scholar 

  20. Gacek, A., Backes, J., Whalen, M.W., Cofer, D.: AGREE Users Guide (2014). http://github.com/smaccm/smaccm

  21. Gómez, R., Bowman, H.: Efficient detection of zeno runs in timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 195–210. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Gafni, V., Benveniste, A., Caillaud, B., Graf, S., Josko, B.: Contract specification language (CSL). Technical report, SPEEDS Deliverable D.2.5.4 (2008)

    Google Scholar 

  23. Pike, L.: Modeling time-triggered protocols and verifying their real-time schedules. In: Formal Methods in Computer-Aided Design, pp. 231–238 (2007)

    Google Scholar 

  24. Sorea, M., Dutertre, B., Steiner, W.: Modeling and verification of time-triggered communication protocols. In: 2008 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing (ISORC), pp. 422–428. IEEE (2008)

    Google Scholar 

  25. Li, W., Grard, L., Shankar, N.: Design and verification of multi-rate distributed systems. In: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 20–29 (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Rockwell Collins, Bloomington, MN, 55438, USA

    John D. Backes & Andrew Gacek

  2. University of Minnesota, Minneapolis, MN, 55455, USA

    Michael W. Whalen & John Komp

Authors
  1. John D. Backes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael W. Whalen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andrew Gacek
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. John Komp
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to John D. Backes .

Editor information

Editors and Affiliations

  1. University of Minnesota, Minneapolis, Minnesota, USA

    Sanjai Rayadurgam

  2. NASA Ames Research Center , Moffett Field, California, USA

    Oksana Tkachuk

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Backes, J.D., Whalen, M.W., Gacek, A., Komp, J. (2016). On Implementing Real-Time Specification Patterns Using Observers. In: Rayadurgam, S., Tkachuk, O. (eds) NASA Formal Methods. NFM 2016. Lecture Notes in Computer Science(), vol 9690. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40648-0_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40647-3

  • Online ISBN: 978-3-319-40648-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation