More Web Proxy on the site http://driver.im/

research-article

Open access

Verification of ${EB}^{3}$ specifications using CADP

Authors:

Dimitris Vekris,

Frédéric Lang,

Radu MateescuAuthors Info & Claims

Formal Aspects of Computing, Volume 28, Issue 1

Pages 145 - 178

https://doi.org/10.1007/s00165-016-0362-6

Published: 01 March 2016 Publication History

Abstract

{E B}^{3}

is a specification language for information systems. The core of the

{E B}^{3}

language consists of process algebraic specifications describing the behaviour of the entities in a system, and attribute function definitions describing the entity attributes. The verification of

{E B}^{3}

specifications against temporal properties is of great interest to users of

{E B}^{3}

. In this paper, we propose a translation from

{E B}^{3}

to LOTOS NT (LNT for short), a value-passing concurrent language with classical process algebra features. Our translation ensures the one-to-one correspondence between states and transitions of the labelled transition systems corresponding to the

{E B}^{3}

and LNT specifications. We automated this translation with the

{E B}^{3} 2 L N T

tool, thus equipping the

{E B}^{3}

method with the functional verification features available in the CADP toolbox.

References

References

[1]

Abdulla PA, Bouajjani A, Jonsson B, Nilsson M (1999) Handling global conditions in parameterized system verification. In: Proceedings of CAV, LNCS, vol 1633. Springer, Berlin, pp 134–145

[2]

Abrial JR The B-book—assigning programs to meanings 2005 Cambridge Cambridge University Press

[3]

Abrial JR Modeling in event-B: system and software engineering 2010 Cambridge Cambridge University Press

[4]

Barradas HR, Bert D (2002) Specification and proof of liveness properties under fairness assumptions in B event systems. In: Proceedings of integrated formal methods, LNCS, vol 2335. Springer, Berlin, pp 360–379

[5]

Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Workshop on Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol 1579. Springer, Berlin, pp 193–207

[6]

Bellegarde F, Chouali S, Julliand J (2002) Verification of dynamic constraints for B event systems under fairness assumptions. In: ZB 2002: formal specification and development in Z and B, LNCS, vol 2272. Springer, Berlin, pp 477–496

[7]

Bergstra JA, Ponse A, and Smolka SA Handbook of process algebra 2001 Amsterdam Elsevier

[8]

Bergstra JA and Klop JW Algebra of communicating processes with abstraction TCS 1985 37 77-121

[9]

Chossart R (2010) Évaluation d’outils de vérification pour les spécifications de systèmes d’information. Master’s thesis, Université de Sherbrooke

[10]

ClearSy. Atelier B. http://www.atelierb.societe.com

[11]

Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, and Tacchella A NuSMV 2: an opensource tool for symbolic model checking 2002 Berlin Springer

[12]

Champelovier D, Clerc X, Garavel H, Guerte Y, McKinty C, Powazny V, Lang F, Serwe W, and Smeding G Reference manual of the LOTOS NT to LOTOS translator—version 5.4 2011 France INRIA/VASY

[13]

Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications J ACM Trans Program Lang Syst, vol 8. Springer, Berlin, pp 244–263

[14]

Emerson EA, Lei CL (1986) Efficient model checking in fragments of the propositional Mu-calculus. In: Proceedings of logic in computer science, pp 267–278

[15]

Evans N, Treharne H, Laleau R, Frappier M (2004) How to verify dynamic properties of information systems. In: Workshop of software engineering and formal, methods, pp 416–425

[16]

Frappier M, Fraikin B, Chossart R, Chane-Yack-Fa R, Ouenzar M (2010) Comparison of model checking tools for information systems. In: Proceedings of ICFEM, LNCS, vol 6447. Springer, Berlin, pp 581–596

[17]

Formal Systems (Europe) Ltd. Failures-divergences refinement. FDR2 User Manual 1997

[18]

Frappier M and St.-Denis R

{E B}^{3}

an entity-based black-box specification method for information systems J Softw Syst Model, vol 2 2003 Berlin Springer 134-149

[19]

Garavel H, Lang F, Mateescu R, Serwe W (2011) CADP 2010: a toolbox for the construction and analysis of distributed processes. In: Proceedings of tools and algorithms for the construction and analysis of systems, LNCS, vol 6605. Springer, Berlin, pp 372–387

[20]

F. Gervais. Combinaison de spécifications formelles pour la modélisation des systèmes d’information. PhD thesis, Université de Sherbrooke, 2006

[21]

J. Groslambert. Verification of LTL on B Event System. Technical report, 2006

[22]

F. Gervais, M. Frappier, R. Laleau. Synthesizing B Specifications from

{E B}^{3}

Attribute Definitions. In Proceedings of Integrated Formal Methods, LNCS vol. 3771, pages 207–226 Springer, 2005

[23]

Gervais F, Frappier M, Laleau R (2006) Refinement of

{E B}^{3}

process patterns into B specifications. In: Proceedings of formal specification and development in B, LNCS, vol 4355. Springer, Berlin, pp 201–215

[24]

Hoare CAR Communicating sequential processes Commun ACM 1978 21 666-677

Digital Library

[25]

Hoang T-S, Abrial T-S (2011) Reasoning about liveness properties in Event-B. In: Proceedings of formal engineering methods, LNCS vol 6991, pp 456–471

[26]

Holzmann GJ The spin model checker: primer and reference manual 2004 Boston Addison-Wesley

Digital Library

[27]

Jackson D Software abstractions 2006 New York MIT Press

Digital Library

[28]

Jiague ME, Frappier M, Gervais F, Konopacki P, Laleau R, Milhau J, St-Denis R (2010) Model-driven engineering of functional security policies. In: Proceedings of international conference on enterprise information, pp 374–379

[29]

ISO/IEC (2001) Enhancements to LOTOS (E-LOTOS). International Standard number 15437:2001, International Organization for Standardization—information technology, Genève

[30]

Leuschel M, Butler M (2003) ProB: a model checker for B. In: Proceedings of symposium on formal methods, LNCS, vol 2805. Springer, Berlin, pp 855–874

[31]

Kozen D Results on the propositional

μ

-calculus TCS 1983 27 333-354

[32]

Leuschel M, Massart M, Currie A (2000) How to make FDR spin: LTL model checking of CSP by refinement. Technical report

[33]

Morgan CC Programming from specifications 1998 Amsterdam Prentice Hall

[34]

Mammar A and Frappier M Proof-based verification approaches for dynamic properties: application to the information system domain J Formal Asp Comput 2015 27 335-374

Digital Library

[35]

Milhau J, Idani A, Laleau R, Labiadh MA, Ledru Y, Frappier M (2011) Combining UML, ASTD and B for the formal specification of an access control filter. J Innov Syst Softw Eng 7:303–313. Springer, Berlin

[36]

Mateescu R, Thivolle D (2008) A model checking language for concurrent value-passing systems. In: Proceedings of formal methods, LNCS, vol 5014. Springer, Berlin, pp 148–164

[37]

Pnueli A (1977) The temporal logic of programs. J. Found. Comput. Sci., vol 18. Springer, Berlin, pp 46–57

[38]

Queille J-P and Sifakis J Fairness and related properties in transition systems-a temporal logic to deal with fairness J Acta Informatica 1983 19 195-220

Digital Library

[39]

Streett R Propositional dynamic logic of looping and converse Inf Contr 1982 54 121-141

[40]

Schneider S, Treharne H (2005) CSP theorems for communicating B machines. J Formal Asp Comput, vol 17. Springer, Berlin, pp 390–422

[41]

Schneider S, Treharne H, Wehrheim H, Williams DM (2014) Managing LTL properties in event-B refinement. In: Proceedings of integrated formal methods. Springer, Berlin, pp 221–237

[42]

Treharne H, Schneider S, Bramble M (2003) Composing specifications using communication. In: Proceedings of ZB, LNCS, vol 2651. Springer, Berlin, pp 55–78

[43]

Vekris D (2014) Verification of

{E B}^{3}

specifications with the aid of model-checking techniques. https://tel.archives-ouvertes.fr/tel-01140261/document. PhD thesis, Université de Paris-Créteil

[44]

Vekris D, Dima C (2013) Efficient operational semantics for

{E B}^{3}

for verification of temporal properties. In: Proceedings of fundamentals of software engineering, LNCS, vol 8161, pp 133–149. Springer, Berlin

[45]

Vekris D, Lang F, Dima C, Mateescu R (2013) Verification of

{E B}^{3}

specifications using CADP. In: Proceedings of integrated formal methods, LNCS, vol 7940. Springer, Berlin, pp 61–76

Cited By

Di Stefano LLang F(2021)Verifying Temporal Properties of Stigmergic Collective Systems Using CADPLeveraging Applications of Formal Methods, Verification and Validation10.1007/978-3-030-89159-6_29(473-489)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-89159-6_29
Chane-Yack-Fa RFrappier MMammar AFinkel A(2018)Parameterized verification of monotone information systemsFormal Aspects of Computing10.1007/s00165-018-0460-830:3-4(463-489)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s00165-018-0460-8

Index Terms

Verification of ${EB}^{3}$ specifications using CADP

Index terms have been assigned to the content through auto-classification.

Recommendations

Model Checking Complete Requirements Specifications Using Abstraction

Although model checking has proven remarkably effective in detecting errors in hardware designs, its success in the analysis of software specifications has been limited. Model checking algorithms for hardware verification commonly use Binary Decision ...
Model checking for ACL compliance verification
AAMAS '03: Proceedings of the second international joint conference on Autonomous agents and multiagent systems

The problem of checking that agents correctly implement the semantics of an agent communication language has become increasingly important as agent technology makes its transition from the research laboratory to field-tested applications. In this paper, ...
Kripke modelling and verification of temporal specifications of a multiple UAV system

A verifiable multiple UAV system cooperatively monitoring a road network is presented in this paper. The focus is on formal modelling and verification which can guarantee correctness of concurrent reactive systems such as multi-UAV systems. Kripke ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 28, Issue 1

Mar 2016

174 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2016.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 March 2016

Accepted: 27 January 2016

Received: 01 December 2013

Published in FAC Volume 28, Issue 1

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
67
Total Downloads

Downloads (Last 12 months)40
Downloads (Last 6 weeks)12

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Di Stefano LLang F(2021)Verifying Temporal Properties of Stigmergic Collective Systems Using CADPLeveraging Applications of Formal Methods, Verification and Validation10.1007/978-3-030-89159-6_29(473-489)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-89159-6_29
Chane-Yack-Fa RFrappier MMammar AFinkel A(2018)Parameterized verification of monotone information systemsFormal Aspects of Computing10.1007/s00165-018-0460-830:3-4(463-489)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s00165-018-0460-8

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents