Skip to main content

Increasing Dependability by Agent-Based Model-Checking During Run-Time

  • Chapter
  • First Online:
  • 1286 Accesses

Part of the book series: Studies in Computational Intelligence ((SCI,volume 640))

Abstract

Agent-oriented software engineering (AOSE) is a paradigm for distributing intelligent control mechanisms (ICM) within an automated production system (aPS). Benefits resulting from AOSE have been surveyed in many applications as route-finding, plug-and-produce techniques and also in the control of Smart Grids. To ensure safe functionalities, i.e. dependability or uptime, of distributed technical systems for instance by conducting simulation, virtual commissioning, the execution of test cases and model-checking are commonly investigated in aPS during the design phase. In this paper we analyze an automatic diagnostic method to increase dependability by using model-checking during run-time, based on discretized models of the mechanical plant as well as models of the PLC software. Consequently the algorithm is incorporated into a software agent and logically coupled to a particular aPS module. Thus, the dependability for introducing novel product types, which have not been involved in the design process, could be increased. The evaluation of our approach is shown at a small lab-scale production system by searching for counter-examples of combinations with control actions and work piece (WP) types with modified mass, that may lead to a production halt.

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

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.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

Learn about institutional subscriptions

Notes

  1. 1.

    Standards for interoperability among software agent platforms (FIPA), http://www.fipa.org, retrieved on 8/17/2015.

  2. 2.

    http://www.mathworks.com, retrieved on 2/19/2016.

References

  1. Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52, 74 (2009)

    Article  Google Scholar 

  2. Silva, B.I., Stursberg, O., Krogh, B.H., Engell, S.: An assessment of the current status of algorithmic approaches to the verification of hybrid systems. In: Proceedings of the 40th IEEE Conference on Decision Control (Cat. No.01CH37228), vol. 3, pp. 2867–2874 (2001)

    Google Scholar 

  3. Stursberg, O., Lohmann, S., Engell, S.: Improving dependability of logic controllers by algorithmic verification. In: IFAC World Congress 2005, pp. 104–109 (2005)

    Google Scholar 

  4. Greifeneder, J., Frey, G.: Probabilistic hybrid automata with variable step width applied to the anaylsis of networked automation systems. Discret. Syst. Des. 3, 283–288 (2006)

    Google Scholar 

  5. Greifeneder, J., Liu, L., Frey, G.: Comparing simulative and formal methods for the analysis of response times in networked automation systems. In: IFAC World Congress 2008, vol. 1, p. O3 (2008)

    Google Scholar 

  6. Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. Comput. Perform. Eval. Model. Tech. Tools 2324, 200–204 (2002)

    Article  MATH  Google Scholar 

  7. Schlich, B., Kowalewski, S.: Model checking C source code for embedded systems. Int. J. Softw. Tools Technol. Transf. 11, 187–202 (2009)

    Article  Google Scholar 

  8. Biallas, S., Kowalewski, S., Stattelmann, S., Schlich, B.: Efficient handling of states in abstract interpretation of industrial programmable logic controller code. In: Workshop on Discrete Event Systems (WODES 2014), pp. 12–17, Cachan, France (2014)

    Google Scholar 

  9. Kowalewski, S., Engell, S., Preußig, J., Stursberg, O.: Verification of logic controllers for continuous plants using timed condition/event-system models. Automatica 35, 505–518 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  10. Santiago, I.B., Faure, J.-M.: From fault tree analysis to model checking of logic controllers. In: IFAC World Congress 2005, pp. 86–91 (2005)

    Google Scholar 

  11. Machado, J.M., Denis, B., Lesage, J.J., Faure, J.M., Ferreira Da Silva, J.C.L.: Logic controllers dependability verification using a plant model. In: Discrete Event Systems, vol. 3, pp. 37–42 (2006)

    Google Scholar 

  12. Wooldridge, M., Jennings, N.: Intelligent Agents: Theory and Practice (1995)

    Google Scholar 

  13. Colombo, A., Schoop, R., Neubert, R.: An agent-based intelligent control platform for industrial holonic manufacturing systems. IEEE Trans. Ind. Electron. 53, 322–337 (2006)

    Article  Google Scholar 

  14. Poslad, S.: Specifying protocols for multi-agent systems interaction. In: ACM Trans. Auton. Adapt. Syst. 2, 15 (2007)

    Google Scholar 

  15. Leitao, P., Marik, V., Vrba, P.: Past, present, and future of industrial agent applications. IEEE Trans. Ind. Inf. 9, 2360–2372 (2013)

    Article  Google Scholar 

  16. Schütz, D., Wannagat, A., Legat, C., Vogel-Heuser, B.: Development of plc-based software for increasing the dependability of production automation systems. IEEE Trans. Ind. Inf. 9, 2397–2406 (2013)

    Article  Google Scholar 

  17. Wooldridge, M.: An Introduction to Multiagent Systems, 2nd edn. Wiley, New York (2009)

    Google Scholar 

  18. Younis, M.B., Frey, G.: Formalization of existing plc programs: a survey. In: CESA 2003, Lille (France), Paper no. S2-R. -00–0239 (2003)

    Google Scholar 

  19. Schlich, B., Brauer, J., Wernerus, J., Kowalewski, S.: Direct model checking of PLC programs in IL. In: 2nd IFAC Workshop on Dependable Control of Discrete Systems, pp. 28–33 (2009)

    Google Scholar 

  20. Schlich, B.: Model Checking of Software for Microcontrollers (2008)

    Google Scholar 

  21. Vogel-Heuser, B., Legat, C., Folmer, J., Feldmann, S.: Researching evolution in industrial plant automation: scenarios and documentation of the pick and place unit (2014)

    Google Scholar 

Download references

Acknowledgment

We thank the German Research Foundation (DFG) for funding this project as part of the Priority Programme SPP 1593: Design for Future—Managed Software Evolution.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Sebastian Rehberger .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Rehberger, S., Aicher, T., Vogel-Heuser, B. (2016). Increasing Dependability by Agent-Based Model-Checking During Run-Time. In: Borangiu, T., Trentesaux, D., Thomas, A., McFarlane, D. (eds) Service Orientation in Holonic and Multi-Agent Manufacturing. Studies in Computational Intelligence, vol 640. Springer, Cham. https://doi.org/10.1007/978-3-319-30337-6_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-30337-6_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-30335-2

  • Online ISBN: 978-3-319-30337-6

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics