Top

Published in:

2018 | OriginalPaper | Chapter

Towards a Hybrid Verification Approach

Authors : Nahla Elaraby, Eva Kühn, Anita Messinger, Sophie Therese Radschek

Published in: Software Technologies: Applications and Foundations

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Verification methods have limitations rooted in their methodological approach. Different methods can be more appropriate in verifying some type of properties than others. We propose a “Hybrid Verification” scheme that verifies different properties using different verification methods and supports a unified specification interface, based on a suitable coordination model. Identifying appropriate verification methods for each property to be verified is a necessary prerequisite for this approach. This work introduces a categorization of properties to be verified and a corresponding mapping to suitable verification methods in accordance with and discussing existing literature. A unified modeling methodology for various assertions based on a coordination model is presented. A generic use cases from the railway domain is used to show the applicability of the proposed Hybrid Verification scheme.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Multi-agent Systems with Virtual Stigmergy

next chapter Using Reinforcement Learning to Handle the Runtime Uncertainties in Self-adaptive Software

Available only for authorised users

http://www.loponode.org, funded by the Austrian Federal Railways (ÖBB Infra).

http://www.era.europa.eu/core-activities/ertm.

read is also denoted as copy, and take as move.

Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRef

Abrial, J.R., Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)MATH

Agha, G.A.: ACTORS: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1990)

Barthe, G., et al.: Preservation of proof obligations for hybrid verification methods. In: 6th IEEE International Conference on Software Engineering and Formal Methods, pp. 127–136 (2008)

Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48119-2_22CrossRef

Behrend, J., et al.: Optimized hybrid verification of embedded software. In: 15th Latin American Test Workshop (LATW), pp. 1–6 (2014)

Bienmüller, T., Damm, W., Wittke, H.: The Statemate verification environment. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 561–567. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_45CrossRefMATH

Butler, M.: A system-based approach to the formal development of embedded controllers for a railway. Des. Autom. Embed. Syst. 6(4), 355–366 (2002)MathSciNetCrossRef

Campos, S., et al.: Verus: a tool for quantitative analysis of finite-state real-time systems. In: ACM SIGPLAN 1995 Workshop on Languages, Compilers and Tools for Real-time Systems. LCTES, pp. 70–78 (1995)

10.

Campos, S., Clarke, E.: The verus language: representing time efficiently with BDDs. In: Bertran, M., Rus, T. (eds.) ARTS 1997. LNCS, vol. 1231, pp. 64–78. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63010-4_5CrossRef

11.

Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Model checking safety critical software with SPIN: an application to a railway interlocking system. In: Ehrenberger, W. (ed.) SAFECOMP 1998. LNCS, vol. 1516, pp. 284–293. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49646-7_22CrossRef

12.

Claessen, K.: Safety property verification of cyclic synchronous circuits. Electron. Notes Theor. Comput. Sci. 88, 55–69 (2004)CrossRef

13.

Clarke, E.M., Schlingloff, B.H.: Model checking. In: Handbook of Automated Reasoning, pp. 1635–1790. Elsevier (2001)

14.

Craß, S., Kühn, E., Salzer, G.: Algebraic foundation of a data model for an extensible space-based collaboration protocol. In: International Database Engineering and Applications Symposium (IDEAS), pp. 301–306. ACM (2009)

15.

Damm, W., Klose, J.: Verification of a radio-based signaling system using the STATEMATE verification environment. Formal Methods Syst. Des. 19(2), 121–141 (2001)CrossRef

16.

Drusinky, D., Shing, M.T.: Verification of timing properties in rapid system prototyping. In: 14th IEEE International Workshop on Rapid System Prototyping, pp. 47–53 (2003)

17.

Du, Q., et al.: High availability verification framework for OpenStack based on fault injection. In: 11th International Conference on Reliability, Maintainability and Safety (ICRMS), pp. 1–7 (2016)

18.

Feng, C., et al.: Complexity and vulnerability of high-speed rail network in China. In: 236th Chinese Control Conference (CCC), pp. 10034–10039 (2017)

19.

Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT 2010, pp. 107–115. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-14261-1_11CrossRef

20.

Gelernter, D.: Generative communication in linda. ACM Trans. Program. Lang. Syst. (TOPLAS) 7(1), 80–112 (1985)CrossRef

21.

Gelernter, D., Carriero, N.: Coordination languages and their significance. Commun. ACM (CACM) 35(2), 96–107 (1992)CrossRef

22.

Glosser, R.J., et al.: Black channel communications apparatus and method, US Patent, WO2016039737, GE Intelligent Platorms Inc. (2016)

23.

Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, New York City (1998)

24.

Hazelhurst, S., et al.: A hybrid verification approach: getting deep into the design. In: Design Automation Conference (IEEE Cat. No. 02CH37324), pp. 111–116 (2002)

25.

James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Treharne, H., Wang, X.: OnTrack: the railway verification toolset. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 294–296. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_21CrossRef

26.

James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. ECEASST 35 (2010)

27.

Jrjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005). https://doi.org/10.1007/b137706CrossRef

28.

Kaneko, S., et al.: Experimental verification on the prediction of the trend in radio resource availability in cognitive radio. In: IEEE 66th Vehicular Technology Conference, pp. 1568–1572 (2007)

29.

Kang, K.C., Ko, K.I.: Formalization and verification of safety properties of statechart specifications. In: Asia-Pacific Software Engineering Conference, pp. 16–27 (1996)

30.

Khan, U., et al.: Real time modeling of interlocking control system of Rawalpindi Cantt train yard. In: 13th International Conference on Frontiers of Information Technology (FIT), pp. 347–352. IEEE (2015)

31.

Kühn, E.: Peer Model White Paper. Technical report, TU Wien (2012–2018)

32.

Kühn, E.: Reusable coordination components: reliable development of cooperative information systems. Int. J. Coop. Inf. Syst. (IJCIS) 25(4) (2016)CrossRef

33.

Kühn, E.: Flexible transactional coordination in the peer model. In: Dastani, M., Sirjani, M. (eds.) FSEN 2017. LNCS, vol. 10522, pp. 116–131. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68972-2_8CrossRef

34.

Kühn, E., et al.: Introducing the concept of customizable structured spaces for agent coordination in the production automation domain. In: 8th International Conference on Autonomous Agents and Multiagent System (AAMAS), IFAAMAS, pp. 625–632 (2009)

35.

Kühn, E., Craß, S., Joskowicz, G., Marek, A., Scheller, T.: Peer-based programming model for coordination patterns. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 121–135. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38493-6_9CrossRef

36.

Kühn, E., Radschek, S.T.: An initial user study comparing the readability of a graphical coordination model with Event-B notation. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 574–590. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74781-1_38CrossRef

37.

Kühn, E., Radschek, S.T., Elaraby, N.: Distributed coordination runtime assertions for the peer model. In: Di Marzo Serugendo, G., Loreti, M. (eds.) COORDINATION 2018. LNCS, vol. 10852, pp. 200–219. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92408-3_9CrossRef

38.

Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46CrossRef

39.

Lidman, J., Mckee, S.A.: Verifying reliability properties using the hyperball abstract domain. ACM Trans. Program. Lang. Syst. 40(1), 3:1–3:29 (2017)CrossRef

40.

Moebius, N., Stenzel, K., Reif, W.: Formal verification of application-specific security properties in a model-driven approach. In: Massacci, F., Wallach, D., Zannone, N. (eds.) ESSoS 2010. LNCS, vol. 5965, pp. 166–181. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11747-3_13CrossRef

41.

Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Technische Hochschule Darmstadt (1962)

42.

Ribeiro, F.G.C., et al.: Guidelines for using MARTE profile packages considering concerns of real-time embedded systems. In: 15th International Conference on Industrial Informatics (INDIN), pp. 917–922 (2017)

43.

Sener, I., et al.: Specification and formal verification of safety properties in point automation system by using timed-arc Petri nets. In: 19th IFAC World Congress. IFAC Proceedings Volumes, vol. 47, no. 3, pp. 12140–12145 (2014)CrossRef

44.

Stothert, A., MacLeod, I.: Modelling and verifying timing properties in distributed computer control systems. In: 13th IFAC Workshop on Distributed Computer Control Systems (DCCS). IFAC Proceedings Volumes, vol. 28, no. 22, pp. 25–30 (1995)CrossRef

45.

Thapa, V., Song, E., Kim, H.: An approach to verifying security and timing properties in UML models. In: 15th IEEE International Conference on Engineering of Complex Computer Systems, pp. 193–202 (2010)

46.

Wang, L., Cai, F.: Reliability analysis for flight control systems using probabilistic model checking. In: 8th IEEE International Conference on Software Engineering and Service Science (ICSESS), pp. 161–164 (2017)

47.

Winter, K., et al.: Tool support for checking railway interlocking designs. In: Tenth Australian Workshop on Safety-Related Programmable Systems (SCS). CRPIT, ACS, vol. 55, pp. 101–107 (2005)

Title: Towards a Hybrid Verification Approach
Authors: Nahla Elaraby
Eva Kühn
Anita Messinger
Sophie Therese Radschek
Publisher: Springer International Publishing
Book: Software Technologies: Applications and Foundations
Print ISBN: 978-3-030-04770-2

Electronic ISBN: 978-3-030-04771-9

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-04771-9_27

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner