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

Article

Model Checking Contracts – A Case Study

Authors:

Cristian Prisacariu,

Gerardo SchneiderAuthors Info & Claims

Automated Technology for Verification and Analysis: 5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings

Pages 82 - 97

https://doi.org/10.1007/978-3-540-75596-8_8

Published: 15 March 2023 Publication History

Abstract

Contracts are agreements between distinct parties that determine rights and obligations on their signatories, and have been introduced in order to reduce risks and to regulate inter-business relationships. In this paper we show how a conventional contract can be written in the contract language, model the contract and verify properties of the model using the NuSMV model checking tool.

References

[1]

Biere A. Grumberg O. mu-cke - efficient mu-calculus model checking CAV 1997 1997 Heidelberg Springer 468-471

[2]

Bradfield J. and Stirling C. Modal Logics and Mu-Calculi: an Introduction 2001 Amsterdam Elsevier 293-330

[3]

Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10²⁰ states and beyond. In: LICS 1990, pp. 428–439 (1990)

[4]

Cimatti A., Clarke E., Giunchiglia E., Giunchiglia F., Pistore M., Roveri M., Sebastiani R., and Tacchella A. Brinksma E. and Larsen K.G. NuSMV 2: An OpenSource Tool for Symbolic Model Checking CAV 2002 2002 Heidelberg Springer 359-364

[5]

Daskalopulu, A.: Model checking contractual protocols. In: JURIX 2000, Frontiers in Artificial Intelligence and Applications Series, pp. 35–47 (2000)

[6]

Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. In: STOC 1977, pp. 286–294 (1977)

[7]

Holzmann G. The Spin Model Checker, Primer and Reference Manual 2003 Reading Addison-Wesley

[8]

Kozen D. Results on the propositional mu-calculus Theor. Comput. Sci. 1983 27 333-354

[9]

Mateescu R. and Sighireanu M. Efficient on-the-fly model-checking for regular alternation-free mu-calculus Sci. Comput. Program. 2003 46 255-281

[10]

McMillan K.L. Symbolic Model Checking 1993 Dordrecht Kluwer Academic Publishers

[11]

McNamara P. Deontic logic Handbook of the History of Logic 2006 Amsterdam North-Holland Publishing 197-289

[12]

Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57 (1977)

[13]

Prisacariu C. and Schneider G. Bonsangue M.M. and Johnsen E.B. A formal language for electronic contracts FMOODS 2007 2007 Heidelberg Springer 174-189

[14]

Rozier K.Y. and Vardi M.Y. Bosnacki D. and Edelkamp S. Ltl satisfiability checking SPIN 2007 2007 Heidelberg Springer 182-200

[15]

Solaiman E., Molina-Jiménez C., and Shrivastava S.K. Orlowska M.E., Weerawarana S., Papazoglou M.M.P., and Yang J. Model checking correctness properties of electronic contracts ICSOC 2003 2003 Heidelberg Springer 303-318

Cited By

Parvizimosaed ARoveri MRasti AAmyot DLogrippo LMylopoulos JSyriani ESahraoui H(2022)Model-checking legal contracts with SymboleoPCProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems10.1145/3550355.3552449(278-288)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550355.3552449

Index Terms

Model Checking Contracts – A Case Study
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Semantics and reasoning

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

Recommendations

Model Checking with SAT-Based Characterization of ACTL Formulas
Formal Methods and Software Engineering
Abstract
Bounded semantics of LTL with existential interpretation and that of ECTL (the existential fragment of CTL), and the characterization of these existentially interpreted properties have been studied and used as the theoretical basis for SAT-based ...
Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code
Hardware and Software: Verification and Testing
Abstract
This paper presents an approach to the efficient verification of embedded systems. Such systems usually operate in uncertain environments, giving rise to a high degree of nondeterminism in the corresponding formal models, which in turn aggravates ...
LTL Model Checking of LLVM Bitcode with Symbolic Data
Mathematical and Engineering Methods in Computer Science
Abstract
The correctness of parallel and reactive programs is often easier specified using formulae of temporal logics. Yet verifying that a system satisfies such specifications is more difficult than verifying safety properties: the recurrence of a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Automated Technology for Verification and Analysis: 5th International Symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007 Proceedings

Oct 2007

474 pages

ISBN:978-3-540-75595-1

DOI:10.1007/978-3-540-75596-8

© Springer-Verlag Berlin Heidelberg 2007.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 15 March 2023

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Parvizimosaed ARoveri MRasti AAmyot DLogrippo LMylopoulos JSyriani ESahraoui H(2022)Model-checking legal contracts with SymboleoPCProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems10.1145/3550355.3552449(278-288)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550355.3552449

View Options

View options

Media

Figures

Other

Tables

View Table of Contents