research-article

Contract-Based Requirement Modularization via Synthesis of Correct Decompositions

Authors:

Thi Thieu Hoa Le,

Roberto Passerone,

Uli Fahrenberg,

Axel LegayAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 15, Issue 2

Article No.: 33, Pages 1 - 26

https://doi.org/10.1145/2885752

Published: 26 February 2016 Publication History

Abstract

In distributed development of modern systems, contracts play a vital role in ensuring interoperability of components and adherence to specifications. It is therefore often desirable to verify the satisfaction of an overall property represented as a contract, given the satisfaction of smaller properties also represented as contracts. When the verification result is negative, designers must face the issue of refining the subproperties and components. This is an instance of the classical synthesis problems: “can we construct a model that satisfies some given specification?” In this work, we propose two strategies enabling designers to synthesize or refine a set of contracts so that their composition satisfies a given contract. We develop a generic algebraic method and show how it can be applied in different contract models to support top-down component-based development of distributed systems.

References

[1]

Sebastian Bauer, Alexandre David, Rolf Hennicker, Kim Guldstrand Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. 2012. Moving from specifications to contracts in component-based design. In Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science, Vol. 7212. Springer, 43--58.

Digital Library

[2]

Albert Benveniste, Benot Caillaud, Alberto Ferrari, Leonardo Mangeruca, Roberto Passerone, and Christos Sofronis. 2008. Multiple viewpoint contract-based specification and design. In Formal Methods for Components and Objects. Lecture Notes in Computer Science, Vol. 5382. Springer, 200--225.

Digital Library

[3]

Luca Benvenuti, Davide Bresolin, Pieter Collins, Alberto Ferrari, Luca Geretti, and Tiziano Villa. 2012. Ariadne: Dominance checking of nonlinear hybrid automata using reachability analysis. In Reachability Problems. Lecture Notes in Computer Science, Vol. 7550. Springer, 79--91.

Digital Library

[4]

L. Benvenuti, A Ferrari, L. Mangeruca, E. Mazzi, R. Passerone, and C. Sofronis. 2008. A contract-based formalism for the specification of heterogeneous systems. In Proceedings of the Forum on Specification, Verification, and Design Languages (FDL’08). 142--147.

[5]

Matteo Bordin and Tullio Vardanega. 2007. Correctness by construction for high-integrity real-time systems: A metamodel-driven approach. In Reliable Software Technologies—Ada Europe 2007. Lecture Notes in Computer Science, Vol. 4498. Springer, 114--127.

Digital Library

[6]

Krishnendu Chatterjee and Thomas A. Henzinger. 2007. Assume-guarantee synthesis. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 4424. Springer, 261--275.

Digital Library

[7]

A. Cimatti and S. Tonetta. 2012. A property-based proof system for contract-based design. In Proceedings of the 2012 38th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA’12). 21--28.

Digital Library

[8]

W. Damm, H. Hungar, B. Josko, T. Peikenkamp, and I. Stierand. 2011. Using contract-based component specifications for virtual integration testing and architecture design. In Proceedings of the Design, Automation, and Test in Europe Conference and Exhibition (DATE’11). 1--6.

[9]

Abhijit Davare, Douglas Densmore, Liangpeng Guo, Roberto Passerone, Alberto L. Sangiovanni-Vincentelli, Alena Simalatsar, and Qi Zhu. 2013. metroII: A design environment for cyber-physical systems. ACM Transactions on Embedded Computing Systems 12, 1s, 49:1--49:31.

Digital Library

[10]

Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. 2009. Methodologies for specification of real-time systems using timed I/O automata. In Formal Methods for Components and Objects. Lecture Notes in Computer Science, Vol. 6286. Springer, 290--310.

Digital Library

[11]

Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. 2010. Timed I/O automata: A complete specification theory for real-time systems. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control (HSCC’10). 10.

Digital Library

[12]

Luca de Alfaro and Thomas A. Henzinger. 2001. Interface automata. In Proceedings of the 8th European Software Engineering Conference Held Jointly with the 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE-9). ACM, New York, NY, 109--120.

Digital Library

[13]

William P. de Roever. 1985. The quest for compositionality. In Proceedings of the IFIP Working Conference on the Role of Abstract Models in Computer Science.

[14]

Edsger W. Dijkstra. 1975. Guarded commands, non-determinacy and a calculus for the derivation of programs. In Proceedings of the International Conference on Reliable Software. ACM, New York, NY, 2--2.13.

Digital Library

[15]

Susanne Graf, Roberto Passerone, and Sophie Quinton. 2014. Contract-based reasoning for component systems with rich interactions. In Embedded Systems Development: From Functional Models to Implementations. Vol. 20. Springer, New York, NY, 139--154.

[16]

A. Iannopollo, P. Nuzzo, S. Tripakis, and A. Sangiovanni-Vincentelli. 2014. Library-based scalable refinement checking for contract-based design. In Proceedings of the Design, Automation, and Test in Europe Conference and Exhibition (DATE’14). 1--6.

Digital Library

[17]

Patricia López Martínez and Tullio Vardanega. 2012. Handling synchronization requirements under separation of concerns in model-driven component-based development. In Reliable Software Technologies—Ada Europe 2012. Lecture Notes in Computer Science, Vol. 7308. Springer, 89--104.

Digital Library

[18]

Leslie Lamport. 1990. Win and sin: Predicate transformers for concurrency. ACM Transactions on Programming Languages and Systems 12, 3, 396--428.

Digital Library

[19]

Thi Thieu Hoa Le and Roberto Passerone. 2014. Refinement-based synthesis of correct contract model decompositions. In Proceedings of the 12th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE’14). 134--143.

[20]

Thi Thieu Hoa Le, Roberto Passerone, Uli Fahrenberg, and Axel Legay. 2016. A tag contract framework for modeling heterogeneous systems. Science of Computer Programming 115--116, 225--246.

Digital Library

[21]

Shang-Wei Lin and Pao-Ann Hsiung. 2011. Counterexample-guided assume-guarantee synthesis through learning. IEEE Transactions on Computers 60, 5, 734--750.

Digital Library

[22]

Barbara Liskov and Jeannette M. Wing. 1994. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems 16, 6, 1811--1841.

Digital Library

[23]

Diego Marmsoler, Alexander Malkis, and Jonas Eckhardt. 2015. A model of layered architectures. In Proceedings of the 12th International Workshop on Formal Engineering Approaches to Software Components and Architectures (FESCA’15). 47--61.

[24]

Bertrand Meyer. 1992. Applying “design by contract.” Computer 25, 10, 40--51.

Digital Library

[25]

Jean-Baptiste Raclet, Eric Badouel, Albert Benveniste, Benoît Caillaud, Axel Legay, and Roberto Passerone. 2011. A modal interface theory for component-based design. Fundamenta Informaticae 108, 1--2, 119--149.

Digital Library

[26]

Alberto Sangiovanni-Vincentelli, Werner Damm, and Roberto Passerone. 2012. Taming Dr. Frankenstein: Contract-based design for cyber-physical systems. European Journal of Control 18, 3, 217--238.

Cited By

Pinto ACorso ASchmerling E(2023)Leveraging Compositional Methods for Modeling and Verification of an Autonomous Taxi System2023 IEEE International Conference on Assured Autonomy (ICAA)10.1109/ICAA58325.2023.00013(34-43)Online publication date: Jun-2023
https://doi.org/10.1109/ICAA58325.2023.00013
Pinto A(2023)Analysis and Design of Uncertain Cyber-Physical SystemsComputation-Aware Algorithmic Design for Cyber-Physical Systems10.1007/978-3-031-43448-8_3(25-53)Online publication date: 25-Aug-2023
https://doi.org/10.1007/978-3-031-43448-8_3
Abbasi KKhan THaq I(2021)Modeling-framework for model-based software engineering of complex Internet of things systemsMathematical Biosciences and Engineering10.3934/mbe.202145818:6(9312-9335)Online publication date: 2021
https://doi.org/10.3934/mbe.2021458
Show More Cited By

Index Terms

Contract-Based Requirement Modularization via Synthesis of Correct Decompositions
1. Computing methodologies
  1. Modeling and simulation
    1. Model development and analysis
      1. Model verification and validation

Recommendations

Refinement-based synthesis of correct contract model decompositions
MEMOCODE '14: Proceedings of the Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign

In distributed development of modern systems, contracts play a vital role in ensuring interoperability of components and adherence to specifications. It is therefore often desirable to verify the satisfaction of an overall property represented as a ...
A tag contract framework for modeling heterogeneous systems

Development of distributed systems can be supported effectively by a contract-based methodology as contracts can ensure interoperability of components and adherence to specifications. Such development can become very complex since distributed systems ...
Contract Monitoring in Agent-Based Systems: Case Study
HoloMAS '09: Proceedings of the 4th International Conference on Industrial Applications of Holonic and Multi-Agent Systems: Holonic and Multi-Agent Systems for Manufacturing

Monitoring of fulfilment of obligations defined by electronic contracts in distributed domains is presented in this paper. A two-level model of contract-based systems and the types of observations needed for contract monitoring are introduced. The ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 15, Issue 2

Special Issue on Innovative Design, Special Issue on MEMOCODE 2014 and Special Issue on M2M/IOT

May 2016

421 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/2888407

Editor:
Sandeep K. Shukla
Indian Institute of Technology, India

Issue’s Table of Contents

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 26 February 2016

Accepted: 01 December 2015

Revised: 01 November 2015

Received: 01 March 2015

Published in TECS Volume 15, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
161
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)1

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Pinto ACorso ASchmerling E(2023)Leveraging Compositional Methods for Modeling and Verification of an Autonomous Taxi System2023 IEEE International Conference on Assured Autonomy (ICAA)10.1109/ICAA58325.2023.00013(34-43)Online publication date: Jun-2023
https://doi.org/10.1109/ICAA58325.2023.00013
Pinto A(2023)Analysis and Design of Uncertain Cyber-Physical SystemsComputation-Aware Algorithmic Design for Cyber-Physical Systems10.1007/978-3-031-43448-8_3(25-53)Online publication date: 25-Aug-2023
https://doi.org/10.1007/978-3-031-43448-8_3
Abbasi KKhan THaq I(2021)Modeling-framework for model-based software engineering of complex Internet of things systemsMathematical Biosciences and Engineering10.3934/mbe.202145818:6(9312-9335)Online publication date: 2021
https://doi.org/10.3934/mbe.2021458
Bakirtzis GFleming CVasilakopoulou C(2021)Categorical Semantics of Cyber-Physical Systems TheoryACM Transactions on Cyber-Physical Systems10.1145/34616695:3(1-32)Online publication date: 11-Jul-2021
https://dl.acm.org/doi/10.1145/3461669
Zhou PZuo DHou KZhang ZDong JLi JZhou H(2019)A Comprehensive Technological Survey on the Dependable Self-Management CPS: From Self-Adaptive Architecture to Self-Management StrategiesSensors10.3390/s1905103319:5(1033)Online publication date: 28-Feb-2019
https://doi.org/10.3390/s19051033
Xu ZNg DEaswaran A(2019)Automatic Generation of Hierarchical Contracts for Resilience in Cyber-Physical Systems2019 IEEE 25th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA)10.1109/RTCSA.2019.8864556(1-11)Online publication date: Aug-2019
https://doi.org/10.1109/RTCSA.2019.8864556
Abbasi KKhan THaq I(2019)Hierarchical Modeling of Complex Internet of Things Systems Using Conceptual Modeling ApproachesIEEE Access10.1109/ACCESS.2019.29309337(102772-102791)Online publication date: 2019
https://doi.org/10.1109/ACCESS.2019.2930933
Íncer Romeo ÍSangiovanni-Vincentelli ALin CKang EHu KZhan N(2018)Quotient for assume-guarantee contractsProceedings of the 16th ACM-IEEE International Conference on Formal Methods and Models for System Design10.5555/3343872.3343881(67-77)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.5555/3343872.3343881
Lago LFerrante OPasserone RFerrari A(2018)Dependability Assessment of SOA-Based CPS With Contracts and Model-Based Fault InjectionIEEE Transactions on Industrial Informatics10.1109/TII.2017.268933714:1(360-369)Online publication date: Jan-2018
https://doi.org/10.1109/TII.2017.2689337
Incer Romeo ISangiovanni-Vincentelli ALin CKang E(2018)Quotient for Assume-Guarantee Contracts2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)10.1109/MEMCOD.2018.8556872(1-11)Online publication date: Oct-2018
https://doi.org/10.1109/MEMCOD.2018.8556872
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents