Towards a Hybrid Verification Approach

Nahla Elaraby; Eva Kühn; Anita Messinger; Sophie Therese Radschek

doi:10.1007/978-3-030-04771-9_27

Federation of International Conferences on Software Technologies: Applications and Foundations

STAF 2018: Software Technologies: Applications and Foundations pp 367-386 | Cite as

Towards a Hybrid Verification Approach

Authors
Authors and affiliations

Nahla Elaraby
Eva Kühn
Anita Messinger
Sophie Therese Radschek

Conference paper

First Online: 06 December 2018

541 Downloads

Part of the Lecture Notes in Computer Science book series (LNCS, volume 11176)

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.

Keywords

System verification Hybrid verification scheme Distributed systems Coordination

This is a preview of subscription content, to check access.

Supplementary material

Open image in new window

Open image in new window

Open image in new window

Appendix A: Peer Model/Graphical Notation in a Nutshell

The following is a brief overview – assembled from [31, 33, 37] – of the features of the Peer Model needed for the use case presented in this paper. The Peer Model is a coordination model that relies on known foundations like shared tuple spaces [20, 21, 34], Actor Model [3], and Petri Nets [41]. It separates coordination logic from business logic and is intended to model reusable coordination solutions. A peer relates to an actor in the Actor Model [3]. It is an autonomous worker with a name; it receives entries (representing messages, events etc.) in an incoming mailbox termed “peer input container” (PIC). Optionally it also possesses a “peer output container” (POC). A container is a tuple space that stores entries that are written, read, or taken (i.e., read and removed) in local transactions. Entries are the units of information passed between peers. An entry has system- and application-defined properties. The coordination behavior of a peer is explicitly modeled with wirings, which have some similarity with Petri Net transitions [41]. A wiring has guards that retrieve entries from containers, and actions that write entries to containers or send them to other peers. In addition, a wiring may call a service which encapsulates application logic. All wirings run concurrently. The arrival of entries in containers triggers the execution of wirings.

Property $prop = (label, val)$. label is a name, and val denotes a value. The property is named after its label.

Entry $e = \mathbb {E}prop$. $\mathbb {E}prop$ is a set of properties $\{prop_1,$ $prop_2,$ $\ldots ,$ $prop_n\}$.

Container $c = (cid, \mathbb {E}, \mathbb {C}oord, \mathbb {C}prop)$. A container stores entries. cid is a unique name, $\mathbb {E}$ a set of entries, $\mathbb {C}oord$ a set of coordinators (see Query below), and $\mathbb {C}prop$ a set of system properties. A container relates to an XVSM container [34]. We differentiate between space containers and internal containers. The former ones support transactions and blocking behavior. Entries are retrieved by a query that necessarily requires the coordination type of the entry.

Query $q = (type, cnt, \mathbb {S}el)$. type is an entry coordination type. cnt is a number, a range, or the keyword ALL or NONE, determining the amount of entries to be selected; default is 1. $\mathbb {S}el$ is a sequence of AND/OR connected selectors. A selector is lent from the XVSM query mechanism [14]. It refers to a container coordinator (e.g. fifo, key, label, any) or is a selection expression involving entry properties, variables and system functions.

Link $l = (c_1, c_2, op, q, \mathbb {E}xpr, \mathbb {L}prop)$. $c_1$ refers to a source and $c_2$ to a target container. op possibilities are³: create (creates new entries and writes them to $c_2$), read (reads entries from $c_1$ and writes them to $c_2$), take (reads and deletes entries from $c_1$ and writes them to $c_2$), delete (reads and deletes entries from $c_1$), and test (checks entries in $c_1$). All operations must fulfill the query q, if it is not empty, on $c_1$. $\mathbb {E}xpr$ is a sequence of expressions that set or get properties of selected entries and/or of variables. $\mathbb {L}prop$ is a set of system properties, like e.g. using flow correlation.

Wiring $w = (wid, \mathbb {G}, \mathbb {S}, \mathbb {A}, wic, \mathbb {W}prop)$. wid is a unique name, $\mathbb {G}$ is a sequence of guard links, $\mathbb {S}$ is a sequence of service links to external services, $\mathbb {A}$ is a sequence of action links, wic is the id of an internal container, and $\mathbb {W}prop$ is a set of system properties. All links are numbered, specifying an execution order which has impact on concurrency and performance. Entries selected by guards are written into wic. Then w calls the services in the specified sequence. Finally, the wiring executes the action links. $c_2$ of a guard and $c_1$ of an action link is wic. There is one dedicated wiring in a peer termed init wiring with its first guard having the identifier “*”; it is fulfilled exactly once, namely when the peer is activated.

Service $s = (sid, app)$. sid is the name of the service and app a reference to the implementation of its application logic (method). A service gets entries from its wiring’s wic as input and emits result entries there (via service links).

Peer $p = (pid, pic, poc, \mathbb {W}id, \mathbb {S}pid, \mathbb {P}prop)$. pid is a unique name, pic and poc are the ids of incoming and outgoing space containers where p receives and delivers entries, $\mathbb {W}id$ is a set of wiring ids, $\mathbb {S}pid$ is a set of ids of sub-peers, and $\mathbb {P}prop$ is a set of system properties.

Peer Model $PM = (\mathbb {P}, \mathbb {W}, \mathbb {C})$. $\mathbb {P}$ is the set of all peers including sub-peers, $\mathbb {W}$ is the set of all wirings, and $\mathbb {C}$ is the set of all containers in the system.

Runtime Assertion Mechanism: In [37], invariant assertions for the Peer Model have been introduced. They are statements about container states. They consist of intra-peer assertions connected to a logic formula by NOT, AND, OR and $\rightarrow $. Intra-peer assertions contain a context and a statement part. The context defines number, type and properties of peers for which the statement must be fulfilled. The statement is a logic formula of container assertions connected by NOT, AND, OR and $\rightarrow $. Container assertions refer to a container where they must hold and a container statement. The container can be the PIC or the POC. The container statement basically is a query on the respective container which may involve local variables (written with a starting $ character). Clearly, due to the nature of runtime assertions, it cannot be guaranteed that all failures are detected. If a strict verification is need, a so-called “history container” HIC can be involved which remembers all events. The mechanism allows for asynchronous distributed runtime reasoning about distributed states with small messaging overhead. The Peer Model supports also the specification of timing properties, but the assertions as presented in [37] cannot yet define constraints on them.

The here proposed Hybrid Verification approach relies on this assertion language to formulate properties and to verify them with respective integrated verification methods. For this, we extend the assertion language by a “future container”, which is a similar concept like the history container. The difference is that assertions using the future container refer to future system states. It is denoted by PIC $^{[t1; t2]}$. This way assertions can refer to entries in the PIC between current time plus t1 and current time plus t2. The implementation of future runtime assertion checking for assertions is part of our future work.

Real-Time Wirings: The Peer Model supports the combination of event- and time-triggered coordination. For the latter, time-triggered wirings and real-time exceptions are defined (see [31] for more details). Time triggered wirings are activated at a specified absolute time (tt.start), and have a defined period (tt.period) and duration(tt.duration).

Graphical Notation: The graphical representation of the Peer Model is shown in Fig. 3, outlining one peer with one wiring that has two links and calls one service (the depiction of service links is skipped in Fig. 3). The guard link connects the peer’s pic with the wirings’s wic, and the action link connects the wiring’s wic with the peer’s poc. Note that the source space container of a guard can also be the peer’s poc or the poc of a sub-peer. Analogously the target space container of an action link can also be the peer’s pic or the pic of a sub-peer. A wiring can have many links that are numbered with G$_1$, $\ldots $, G$_k$, S$_1$, $\ldots $, S$_m$, A$_1$, $\ldots $, A$_n$ (the link ids are not depicted in Fig. 3). A peer can have many wirings.

Sub-wirings that are called as synchronous sub-transactions [33] are denoted with dashed lines.

References

1.
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefGoogle Scholar
2.
Abrial, J.R., Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)zbMATHGoogle Scholar
3.
Agha, G.A.: ACTORS: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1990)Google Scholar
4.
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)Google Scholar
5.
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_22CrossRefGoogle Scholar
6.
Behrend, J., et al.: Optimized hybrid verification of embedded software. In: 15th Latin American Test Workshop (LATW), pp. 1–6 (2014)Google Scholar
7.
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_45CrossRefzbMATHGoogle Scholar
8.
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)MathSciNetCrossRefGoogle Scholar
9.
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)Google Scholar
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_5CrossRefGoogle Scholar
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_22CrossRefGoogle Scholar
12.
Claessen, K.: Safety property verification of cyclic synchronous circuits. Electron. Notes Theor. Comput. Sci. 88, 55–69 (2004)CrossRefGoogle Scholar
13.
Clarke, E.M., Schlingloff, B.H.: Model checking. In: Handbook of Automated Reasoning, pp. 1635–1790. Elsevier (2001)Google Scholar
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)Google Scholar
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)CrossRefGoogle Scholar
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)Google Scholar
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)Google Scholar
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)Google Scholar
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_11CrossRefGoogle Scholar
20.
Gelernter, D.: Generative communication in linda. ACM Trans. Program. Lang. Syst. (TOPLAS) 7(1), 80–112 (1985)CrossRefGoogle Scholar
21.
Gelernter, D., Carriero, N.: Coordination languages and their significance. Commun. ACM (CACM) 35(2), 96–107 (1992)CrossRefGoogle Scholar
22.
Glosser, R.J., et al.: Black channel communications apparatus and method, US Patent, WO2016039737, GE Intelligent Platorms Inc. (2016)Google Scholar
23.
Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, New York City (1998)Google Scholar
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)Google Scholar
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_21CrossRefGoogle Scholar
26.
James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. ECEASST 35 (2010)Google Scholar
27.
Jrjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005). https://doi.org/10.1007/b137706CrossRefGoogle Scholar
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)Google Scholar
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)Google Scholar
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)Google Scholar
31.
Kühn, E.: Peer Model White Paper. Technical report, TU Wien (2012–2018)Google Scholar
32.
Kühn, E.: Reusable coordination components: reliable development of cooperative information systems. Int. J. Coop. Inf. Syst. (IJCIS) 25(4) (2016)CrossRefGoogle Scholar
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_8CrossRefGoogle Scholar
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)Google Scholar
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_9CrossRefGoogle Scholar
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_38CrossRefGoogle Scholar
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_9CrossRefGoogle Scholar
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_46CrossRefGoogle Scholar
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)CrossRefGoogle Scholar
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_13CrossRefGoogle Scholar
41.
Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Technische Hochschule Darmstadt (1962)Google Scholar
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)Google Scholar
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)CrossRefGoogle Scholar
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)CrossRefGoogle Scholar
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)Google Scholar
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)Google Scholar
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)Google Scholar

Copyright information

Authors and Affiliations

Nahla Elaraby
- 1
- 2
Email author
Eva Kühn
- 1
Anita Messinger
- 1
Sophie Therese Radschek
- 1

1.Faculty of InformaticsTU WienViennaAustria
2.Canadian International College – CICCairoEgypt

Towards a Hybrid Verification Approach

Abstract

Keywords

Supplementary material

References

Copyright information

Authors and Affiliations

Personalised recommendations

Cite paper