Article

Counterexample guided synthesis of monitors for realizability enforcement

Authors:

Matthias Güdemann,

Meriem OuederniAuthors Info & Claims

ATVA'12: Proceedings of the 10th international conference on Automated Technology for Verification and Analysis

Pages 238 - 253

https://doi.org/10.1007/978-3-642-33386-6_20

Published: 03 October 2012 Publication History

Abstract

Many of today's software systems are built using distributed services, which evolve in different organizations. In order to facilitate their integration, it is necessary to provide a contract that the services participating in a composition should adhere to. A contract specifies interactions among a set of services from a global point of view. One important problem in a top-down development process is figuring out whether such a contract can be implemented by a set of services, obtained by projection and communicating via message passing. It was only recently shown, that this problem, known as realizability, is decidable if asynchronous communication (communication via FIFO buffers) is considered. It can be verified using the synchronizability property. If the system is not synchronizable, the system is not realizable either. In this paper, we propose a new, automatic approach, which enforces both synchronizability and realizability by generating local monitors through successive equivalence checks and refinement.

References

[1]

Alur, R., Etessami, K., Yannakakis, M.: Realizability and Verification of MSC Graphs. Theoretical Computer Science 331(1), 97-114 (2005)

Digital Library

[2]

Andrews, T.: et al. Business Process Execution Language for Web Services (WSBPEL). BEA Systems, IBM, Microsoft, SAP AG, and Siebel Systems (2005)

[3]

Basu, S., Bultan, T., Ouederni, M.: Deciding Choreography Realizability. In: Proc. of POPL 2012. ACM Press (2012)

Digital Library

[4]

Bultan, T., Fu, X.: Specification of Realizable Service Conversations using Collaboration Diagrams. Service Oriented Computing and Applications 2(1), 27-39 (2008)

[5]

Carbone, M., Honda, K., Yoshida, N.: Structured Communication-Centred Programming for Web Services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2-17. Springer, Heidelberg (2007)

Digital Library

[6]

Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4). INRIA/VASY, 149 pages (2011)

[7]

Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E. A., Sistla, A. P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154-169. Springer, Heidelberg (2000)

Digital Library

[8]

Crouzen, P., Lang, F.: Smart Reduction. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 111-126. Springer, Heidelberg (2011)

Digital Library

[9]

Decker, G., Weske, M.: Local Enforceability in Interaction Petri Nets. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 305-319. Springer, Heidelberg (2007)

Digital Library

[10]

Fu, X., Bultan, T., Su, J.: Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services. Theoretical Computer Science 328(1-2), 19-37 (2004)

Digital Library

[11]

Fu, X., Bultan, T., Su, J.: Synchronizability of Conversations among Web Services. IEEE Transactions on Software Engineering 31(12), 1042-1055 (2005)

Digital Library

[12]

Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P. A., Leino, K. R. M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372-387. Springer, Heidelberg (2011)

Digital Library

[13]

Garavel, H., Mateescu, R.: XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. In: Proc. STTT 1998 (1998)

[14]

Hopcroft, J. E., Ullman, J. D.: Introduction to Automata Theory, Languages and Computation. Addison Wesley (1979)

Digital Library

[15]

Lohmann, N., Wolf, K.: Realizability Is Controllability. In: Laneve, C., Su, J. (eds.) WS-FM 2009. LNCS, vol. 6194, pp. 110-127. Springer, Heidelberg (2010)

Digital Library

[16]

Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148-164. Springer, Heidelberg (2008)

Digital Library

[17]

Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall (1989)

Digital Library

[18]

OMG. Business Process Model and Notation (BPMN) - Version 2.0 (2011)

[19]

Poizat, P., Salaün, G.: Checking the Realizability of BPMN 2.0 Choreographies. In: Proc. of SAC 2012. ACM Press (2012)

Digital Library

[20]

Qiu, Z., Zhao, X., Cai, C., Yang, H.: Towards the Theoretical Foundation of Choreography. In: Proc. of WWW 2007. ACM Press (2007)

Digital Library

[21]

Salaün, G., Bultan, T.: Realizability of Choreographies Using Process Algebra Encodings. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 167-182. Springer, Heidelberg (2009)

Digital Library

[22]

Stengel, Z., Bultan, T.: Analyzing Singularity Channel Contracts. In: Proc. of ISSTA 2009. ACM (2009)

Digital Library

Cited By

Falcone YSalaün G(2021)Runtime Enforcement with Reordering, Healing, and SuppressionSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_3(47-65)Online publication date: 6-Dec-2021
https://dl.acm.org/doi/10.1007/978-3-030-92124-8_3
Dai FChen HQiang ZLiang ZHuang BWang LZhang X(2020)Automatic Analysis of Complex Interactions in Microservice SystemsComplexity10.1155/2020/21287932020Online publication date: 31-Mar-2020
https://dl.acm.org/doi/10.1155/2020/2128793
Najem T(2019)A formal semantics for supporting the automated synthesis of choreography-based architecturesProceedings of the 13th European Conference on Software Architecture - Volume 210.1145/3344948.3344949(51-54)Online publication date: 9-Sep-2019
https://dl.acm.org/doi/10.1145/3344948.3344949
Show More Cited By

Recommendations

Efficient runtime policy enforcement using counterexample-guided abstraction refinement
CAV'12: Proceedings of the 24th international conference on Computer Aided Verification

Stateful security policies--which specify restrictions on behavior in terms of temporal safety properties--are a powerful tool for administrators to control the behavior of untrusted programs. However, the runtime overhead required to enforce them on ...
SAT-based counterexample-guided abstraction refinement

We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" ...
A counterexample guided abstraction refinement framework for verifying concurrent c programs

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ATVA'12: Proceedings of the 10th international conference on Automated Technology for Verification and Analysis

October 2012

434 pages

ISBN:9783642333859

Editors:
Supratik Chakraborty
Indian Institute of Technology, Computer Science and Engineering, Dept. of Computer Science and Engineering, IIT Bombay, Powai, Mumbai, Maharashtra, India
,
Madhavan Mukund
Indian Institute of Technology, Computer Science and Engineering, Dept. of Computer Science and Engineering, Chennai Mathematical Institute, H1, SIPCOT IT Park, Kelambakkam, Siruseri, Tamil Nadu, India

Sponsors

Microsoft Research India: Microsoft Research India
Siemens Technology and Services: Siemens Technology and Services Pvt. Ltd.
Computer Society of India: Computer Society of India
Tata Consultancy Services
IARCS: Indian Association for Research in Computing Science

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 03 October 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Falcone YSalaün G(2021)Runtime Enforcement with Reordering, Healing, and SuppressionSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_3(47-65)Online publication date: 6-Dec-2021
https://dl.acm.org/doi/10.1007/978-3-030-92124-8_3
Dai FChen HQiang ZLiang ZHuang BWang LZhang X(2020)Automatic Analysis of Complex Interactions in Microservice SystemsComplexity10.1155/2020/21287932020Online publication date: 31-Mar-2020
https://dl.acm.org/doi/10.1155/2020/2128793
Najem T(2019)A formal semantics for supporting the automated synthesis of choreography-based architecturesProceedings of the 13th European Conference on Software Architecture - Volume 210.1145/3344948.3344949(51-54)Online publication date: 9-Sep-2019
https://dl.acm.org/doi/10.1145/3344948.3344949
Autili MDi Salle AGallo FPompilio CTivoli MHung CPapadopoulos G(2019)Aiding the realization of service-oriented distributed systemsProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297446(1701-1710)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297446
Autili MDi Salle AGallo FPompilio CTivoli MHaddad HWainwright RChbeir R(2018)Model-driven adaptation of service choreographiesProceedings of the 33rd Annual ACM Symposium on Applied Computing10.1145/3167132.3167287(1441-1450)Online publication date: 9-Apr-2018
https://dl.acm.org/doi/10.1145/3167132.3167287
Akroun LSalaün G(2018)Automated verification of automata communicating via FIFO and bag buffersFormal Methods in System Design10.1007/s10703-017-0285-852:3(260-276)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10703-017-0285-8
Farah ZAit-Ameur YOuederni MTari K(2017)A correct-by-construction model for asynchronously communicating systemsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0421-619:4(465-485)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s10009-016-0421-6
Basu SBultan T(2016)Automated Choreography RepairProceedings of the 19th International Conference on Fundamental Approaches to Software Engineering - Volume 963310.5555/3089458.3089462(13-30)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.5555/3089458.3089462
Lange JTuosto EYoshida N(2015)From Communicating Machines to Graphical ChoreographiesACM SIGPLAN Notices10.1145/2775051.267696450:1(221-232)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2775051.2676964
Lange JTuosto EYoshida NRajamani SWalker D(2015)From Communicating Machines to Graphical ChoreographiesProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2676726.2676964(221-232)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2676726.2676964
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents