Skip to main content
SpringerLink
Log in

Compositional Nonblocking Verification with Always Enabled Events and Selfloop-Only Events

  • Conference paper
  • First Online:
Formal Techniques for Safety-Critical Systems (FTSCS 2013)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 419))

  • 476 Accesses

Abstract

This paper proposes to improve compositional nonblocking verification through the use of always enabled and selfloop-only events. Compositional verification involves abstraction to simplify parts of a system during verification. Normally, this abstraction is based on the set of events not used in the remainder of the system, i.e., in the part of the system not being simplified. Here, it is proposed to exploit more knowledge about the system and abstract events even though they are used in the remainder of the system. Abstraction rules from previous work are generalised, and experimental results demonstrate the applicability of the resulting algorithm to verify several industrial-scale discrete event system models, while achieving better state-space reduction than before.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

References

  1. Åkesson, K., Fabian, M., Flordal, H., Malik, R.: Supremica—an integrated environment for verification, synthesis and simulation of discrete event systems. In: Proceedings of the 8th International Workshop on Discrete Event Systems, WODES ’06, Ann Arbor, MI, USA, pp. 384–385 (2006)

    Google Scholar 

  2. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    Google Scholar 

  3. Brandin, B., Charbonnier, F.: The supervisory control of the automated manufacturing system of the AIP. In: Proceedings of Rensselaer’s 4th International Conference on Computer Integrated Manufacturing and Automation Technology, Troy, NY, USA, pp. 319–324 (1994)

    Google Scholar 

  4. Brandin, B.A., Malik, R., Malik, P.: Incremental verification and synthesis of discrete-event systems guided by counter-examples. IEEE Trans. Control Syst. Technol. 12(3), 387–401 (2004)

    Article  Google Scholar 

  5. Brookes, S.D., Rounds, W.C.: Behavioural equivalence relations induced by programming logics. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 97–108. Springer, Heidelberg (1983)

    Google Scholar 

  6. Cassandras, C.G., Lafortune, S. (eds.): Introduction to Discrete Event Systems, 2nd edn. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  7. De Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes. Theor. Comput. Sci. 34(1–2), 83–133 (1984)

    Article  MATH  Google Scholar 

  8. Eloranta, J.: Minimizing the number of transitions with respect to observation equivalence. BIT 31(4), 397–419 (1991)

    Article  MathSciNet  Google Scholar 

  9. Flordal, H., Malik, R.: Compositional verification in supervisory control. SIAM J. Control Optim. 48(3), 1914–1938 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  10. Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186–6. Springer, Heidelberg (1991)

    Google Scholar 

  11. Hinze, A., Malik, P., Malik, R.: Interaction design for a mobile context-aware system using discrete event modelling. In: Proceedings of the 29th Australasian Computer Science Conference, ACSC ’06, pp. 257–266. Australian Computer Society, Hobart (2006)

    Google Scholar 

  12. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  13. Leduc, R.J.: PLC implementation of a DES supervisor for a manufacturing testbed: an implementation perspective. Master’s thesis. Department of Electrical Engineering, University of Toronto, ON, Canada. http://www.cas.mcmaster.ca/~leduc (1996)

  14. Leduc, R.J.: Hierarchical interface-based supervisory control. Ph.D. thesis, Department of Electrical Engineering, University of Toronto, ON, Canada. http://www.cas.mcmaster.ca/~leduc (2002)

  15. Malik, R., Mühlfeld, R.: A case study in verification of UML statecharts: the PROFIsafe protocol. J. Univ. Comput. Sci. 9(2), 138–151 (2003)

    Google Scholar 

  16. Malik, R.: The language of certain conflicts of a nondeterministic process. Working Paper 05/2010, Department of Computer Science, University of Waikato, Hamilton, New Zealand. http://hdl.handle.net/10289/4108 (2010)

  17. Malik, R., Leduc, R.: Compositional nonblocking verification using generalised nonblocking abstractions. IEEE Trans. Autom. Control 58(8), 1–13 (2013)

    Article  MathSciNet  Google Scholar 

  18. Malik, R., Streader, D., Reeves, S.: Conflicts and fair testing. Int. J. Found. Comput. Sci. 17(4), 797–813 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  19. Milner, R.: Communication and Concurrency. Series in Computer Science. Prentice-Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  20. Pena, P.N., Cury, J.E.R., Lafortune, S.: Verification of nonconflict of supervisors using abstractions. IEEE Trans. Autom. Control 54(12), 2803–2815 (2009)

    Article  MathSciNet  Google Scholar 

  21. Pilbrow, C.: Compositional nonblocking verification with always enabled and selfloop-only events. Working Paper 07/2013, Department of Computer Science, University of Waikato, Hamilton, New Zealand. http://hdl.handle.net/10289/8187 (2013)

  22. Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81–98 (1989)

    Article  Google Scholar 

  23. KorSys Project. http://www4.in.tum.de/proj/korsys/

  24. Song, R.: Symbolic synthesis and verification of hierarchical interface-based supervisory control. Master’s thesis, Department of Computing and Software, McMaster University, Hamilton, ON, Canada. http://www.cas.mcmaster.ca/~leduc (2006)

  25. Su, R., van Schuppen, J.H., Rooda, J.E., Hofkamp, A.T.: Nonconflict check by using sequential automaton abstractions based on weak observation equivalence. Automatica 46(6), 968–978 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  26. Supremica. http://www.supremica.org

  27. Valmari, A.: Compositionality in state space verification methods. In: Billington, J., Reisig, W. (eds.) Application and Theory of Petri Nets 1996. LNCS, vol. 1091, pp. 29–56. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  28. Yi, J., Ding, S., Zhang, M.T., van der Meulen, P.: Throughput analysis of linear cluster tools. In: Proceedings of the 3rd International Conference on Automation Science and Engineering, CASE 2007, Scottsdale, AZ, USA, pp. 1063–1068 (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Waikato, Hamilton, New Zealand

    Colin Pilbrow & Robi Malik

Authors
  1. Colin Pilbrow
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robi Malik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Robi Malik .

Editor information

Editors and Affiliations

  1. AIST, Research Institute for Secure Systems, Amagasaki, Japan

    Cyrille Artho

  2. University of Oslo Department of Informatics, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Pilbrow, C., Malik, R. (2014). Compositional Nonblocking Verification with Always Enabled Events and Selfloop-Only Events. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2013. Communications in Computer and Information Science, vol 419. Springer, Cham. https://doi.org/10.1007/978-3-319-05416-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-05416-2_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-05415-5

  • Online ISBN: 978-3-319-05416-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation