Skip to main content

A Visual Logic for the Description of Highway Traffic Scenarios

  • Conference paper
Complex Systems Design & Management

Abstract

In this paper, we present the syntax and semantics of the visual logic (VL) used to specify (sequences of) traffic situations on the highway. VL was developed in the context of driver assistance system development, and is intended to bridge the (terminology) gap between system engineers and traffic psychologists developing driver assistance systems, and scientists modelling, analysing and verifying such systems. To achieve this goal, the logic is intuitive and simple, thus easy to understand and apply, yet it has a formal, automaton-based semantics which allows to use well-established tools and formalisms for further analysis of the system.

We show how VL can be used to specify scenarios on the highway involving interaction of driver and assistance system, and how it can be used in the context of observer-based verification to analyse and verify the assistance system with respect to these scenarios.

This work was partly supported by Ministry for Science and Culture of Lower Saxony as part of the interdisciplinary research project ”Integrated Modelling for Safe Transportation II” (IMoST2), and by European Commission funding the Large-scale integrating project (IP) proposal under ICT Call 7 (FP7-ICT-2011-7) Designing for Adaptability and evolutioN in System of systems Engineering (DANSE) (No. 287716).

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Allen, J.: Maintaining knowledge about temporal intervals. CACM 26(11), 832–843 (1983)

    Article  MATH  Google Scholar 

  2. Allen, R., Douence, R., Garlan, D.: Specifying and analyzing dynamic software architectures. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 21–37. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  3. Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  4. Bauer, J., Wilhelm, R.: Static analysis of dynamic communication systems by partner abstraction. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 249–264. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Bradbury, J., Cordy, J., Dingel, J., Wermelinger, M.: A survey of self-management in dynamic software architecture specifications. In: Garlan, D., Kramer, J., Wolf, A. (eds.) WOSS, pp. 28–33. ACM (2004)

    Google Scholar 

  6. Brill, M., Damm, W., Klose, J., Westphal, B., Wittke, H.: Live Sequence Charts: An Introduction to Lines, Arrows, and Strange Boxes in the Context of Formal Verification. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 374–399. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Burmester, S., Giese, H., Tichy, M.: Model-driven development of reconfigurable mechatronic systems with mechatronic UML. In: Aßmann, U., Akşit, M., Rensink, A. (eds.) MDAFA 2003. LNCS, vol. 3599, pp. 47–61. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Canal, C., Pimentel, E., Troya, J.: Specification and refinement of dynamic software architectures. In: Donohoe, P. (ed.) WICSA, IFIP Conference Proceedings, vol. 140, pp. 107–126. Kluwer (1999)

    Google Scholar 

  9. Etzien, C., Gezgin, T., Fröschle, S., Henkler, S., Rettberg, A.: Contracts for evolving systems. In: 4th IEEE Workshop on Self-Organizing Real-Time Systems (to appear, 2013)

    Google Scholar 

  10. Gezgin, T., Etzien, C., Henkler, S., Rettberg, A.: Towards a rigorous modeling formalism for systems of systems. In: ISORC Workshops, pp. 204–211. IEEE (2012)

    Google Scholar 

  11. Henkler, S., Hirsch, M., Priesterjahn, C., Schäfer, W.: Modeling and verifying dynamic communication structures based on graph transformations. In: Engels, G., Luckey, M., Schäfer, W. (eds.) Software Engineering. LNI, vol. 159, pp. 153–164. GI (2010)

    Google Scholar 

  12. Henzinger, T.A.: Masaccio: A formal model for embedded components. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 549–563. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Hirsch, D., Inverardi, P., Montanari, U.: Graph grammars and constraint solving for software architecture styles. In: ISAW, pp. 69–72. ACM (1998)

    Google Scholar 

  14. Hirsch, M., Henkler, S., Giese, H.: Modeling collaborations with dynamic structural adaptation in mechatronic UML. In: SEAMS, pp. 33–40. ACM (2008)

    Google Scholar 

  15. Ivancic, F.: Modeling and analysis of hybrid systems. Ph.D. thesis, Univ. of Pennsylvania (2003)

    Google Scholar 

  16. Kemper, S.: SAT-based Verification for Timed Component Connectors. Sciene of Computer Programming 77(7-8), 779–798 (2012), http://www.sciencedirect.com/science/article/pii/S0167642311000499

    Article  MATH  Google Scholar 

  17. Klose, J.: Live sequence charts: A graphical formalism for the specification of communication behaviour. Ph.D. thesis, Universität Oldenburg (2003)

    Google Scholar 

  18. Kramer, J., Magee, J.: Analysing dynamic change in software architectures: a case study. In: CDS, pp. 91–100. IEEE (1998)

    Google Scholar 

  19. Maier, M.: Architecting principles for systems-of-systems. Syst. Eng. 1(4), 267–284 (1998)

    Article  Google Scholar 

  20. Oreizy, P., Medvidovic, N., Taylor, R.: Architecture-based runtime software evolution. In: Torii, K., Futatsugi, K., Kemmerer, R. (eds.) ICSE, pp. 177–186. IEEE CS (1998)

    Google Scholar 

  21. Taentzer, G., Goedicke, M., Meyer, T.: Dynamic change management by distributed graph transformation: towards configurable distributed systems. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) TAGT 1998. LNCS, vol. 1764, pp. 179–193. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  22. UPPAAL: modeling, simulation and verification of real-time systems, http://www.uppaal.com/

  23. Yovine, S.: Kronos: A verification tool for real-time systems. STTT 1(1-2), 123–133 (1997)

    Article  MATH  Google Scholar 

  24. Zhang, J., Cheng, B.: Model-based development of dynamically adaptive software. In: Osterweil, L., Rombach, H., Soffa, M. (eds.) ICSE, pp. 371–380. ACM (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Stephanie Kemper .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Kemper, S., Etzien, C. (2014). A Visual Logic for the Description of Highway Traffic Scenarios. In: Aiguier, M., Boulanger, F., Krob, D., Marchal, C. (eds) Complex Systems Design & Management. Springer, Cham. https://doi.org/10.1007/978-3-319-02812-5_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-02812-5_17

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-02811-8

  • Online ISBN: 978-3-319-02812-5

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics