chapter

Model-checking CSP

Author:

A. W. RoscoeAuthors Info & Claims

A classical mind: essays in honour of C. A. R. Hoare

January 1994

Pages 353 - 378

Published: 11 January 1994 Publication History

Abstract

No abstract available.

Cited By

View all

Bowen J(2022)Review on Theories of Programming: The Life and Works of Tony HoareFormal Aspects of Computing10.1145/356026734:3-4(1-3)Online publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1145/3560267
Gibson-Robinson TArmstrong PBoulgakov ARoscoe A(2016)FDR3International Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0377-y18:2(149-167)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1007/s10009-015-0377-y
Gui LSun JLiu YDong JYoung MXie T(2015)Reliability assessment for distributed systems via communication abstraction and refinementProceedings of the 2015 International Symposium on Software Testing and Analysis10.1145/2771783.2771794(293-304)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1145/2771783.2771794
Show More Cited By

Index Terms

Model-checking CSP
1. Computing methodologies
  1. Concurrent computing methodologies
    1. Concurrent programming languages
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Concurrent programming languages

Recommendations

On the limits of refinement-testing for model-checking CSP
Abstract
Refinement-checking, as embodied in tools like FDR, PAT and ProB, is a popular approach for model-checking refinement-closed predicates of CSP processes. We consider the limits of this approach to model-checking these kinds of predicates. By ...
Compositional CSP Traces Refinement Checking

Compositional verification using assume-guarantee reasoning has recently seen an uprise due to the introduction of automatic techniques for learning assumptions. In this paper, we transfer this technique to a setting with CSP as modelling and property ...
Assumption-Commitment Support for CSP Model Checking

We present a simple formulation of Assumption-Commitment reasoning using CSP. In our formulation, an assumption-commitment style property of a process SYS takes the form COM @?SYS @?ASS, for some 'assumption' and 'commitment' processes ASS and COM. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

A classical mind: essays in honour of C. A. R. Hoare

January 1994

451 pages

ISBN:0132948443

Editor:
A. W. Roscoe
Oxford Univ. Computing Lab., Oxford, UK

Publisher

Prentice Hall International (UK) Ltd.

United Kingdom

Publication History

Published: 11 January 1994

Qualifiers

Chapter

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

63
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Bowen J(2022)Review on Theories of Programming: The Life and Works of Tony HoareFormal Aspects of Computing10.1145/356026734:3-4(1-3)Online publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1145/3560267
Gibson-Robinson TArmstrong PBoulgakov ARoscoe A(2016)FDR3International Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0377-y18:2(149-167)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1007/s10009-015-0377-y
Gui LSun JLiu YDong JYoung MXie T(2015)Reliability assessment for distributed systems via communication abstraction and refinementProceedings of the 2015 International Symposium on Software Testing and Analysis10.1145/2771783.2771794(293-304)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1145/2771783.2771794
Roscoe AHopcroft P(2013)Slow abstraction via priorityTheories of Programming and Formal Methods10.5555/2554641.2554661(326-345)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554641.2554661
Sinnig DChalin PKhendek F(2013)Use case and task modelsACM Transactions on Software Engineering and Methodology10.1145/2491509.249152122:3(1-31)Online publication date: 30-Jul-2013
https://dl.acm.org/doi/10.1145/2491509.2491521
Wei KWoodcock JBurns A(2013)Modelling temporal behaviour in complex systems with TimebandsFormal Methods in System Design10.1007/s10703-013-0193-543:3(520-551)Online publication date: 1-Dec-2013
https://dl.acm.org/doi/10.1007/s10703-013-0193-5
Roscoe AHuang J(2013)Checking noninterference in Timed CSPFormal Aspects of Computing10.1007/s00165-012-0251-625:1(3-35)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.1007/s00165-012-0251-6
Hatcliff JLeavens GLeino KMüller PParkinson M(2012)Behavioral interface specification languagesACM Computing Surveys10.1145/2187671.218767844:3(1-58)Online publication date: 14-Jun-2012
https://dl.acm.org/doi/10.1145/2187671.2187678
Wang TSong SSun JLiu YDong JWang XLi S(2012)More anti-chain based refinement checkingProceedings of the 14th international conference on Formal Engineering Methods: formal methods and software engineering10.1007/978-3-642-34281-3_26(364-380)Online publication date: 12-Nov-2012
https://dl.acm.org/doi/10.1007/978-3-642-34281-3_26
Burns EZhou R(2012)Parallel model checking using abstractionProceedings of the 19th international conference on Model Checking Software10.1007/978-3-642-31759-0_13(172-190)Online publication date: 23-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31759-0_13
Show More Cited By

Abstract

Cited By

Index Terms

Recommendations

On the limits of refinement-testing for model-checking CSP

Compositional CSP Traces Refinement Checking

Assumption-Commitment Support for CSP Model Checking

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations