research-article

A CSP-based framework for the specification, verification, and implementation of adaptive systems

Authors:

Björn Bartels,

Moritz KleineAuthors Info & Claims

SEAMS '11: Proceedings of the 6th International Symposium on Software Engineering for Adaptive and Self-Managing Systems

Pages 158 - 167

https://doi.org/10.1145/1988008.1988030

Published: 23 May 2011 Publication History

Abstract

The process algebra CSP is tailored for the specification and verification of reactive systems. Such systems react upon external stimuli by adjusting their internal behavior, e.g., to recover from errors. Adaptive systems can be regarded as a subclass of reactive systems in the sense that such systems react by adapting to changes propagated by some stimulus. In this paper, we use CSP for the specification, verification and implementation of adaptive systems. This enables us to use standard CSP tools such as FDR, ProB or the CSP-Prover for the verification of such systems. Furthermore, we present an approach for the implementation of systems specified in CSP.

References

[1]

Rasmus Adler, Ina Schaefer, Tobias Schuele, and Eric Vecchié. From model-based design to formal verification of adaptive embedded systems. In Proceedings of the formal engineering methods 9th international conference on Formal methods and software engineering, ICFEM'07, pages 76--95, Berlin, Heidelberg, 2007. Springer-Verlag.

Digital Library

[2]

Robert Allen, Rémi Douence, and David Garlan. Specifying and analyzing dynamic software architectures. In Proceedings of the 1998 Conference on Fundamental Approaches to Software Engineering (FASE'98), Lisbon, Portugal, 1998.

[3]

B. Bartels and S. Glesner. Formal Modeling and Verification of Low-Level Software Programs. In 10th International Conference on Qualtiy Software (QSIC 2010). IEEE Computer Society, July 2010.

Digital Library

[4]

M. Fontaine. Towards Reusable Formal Method Tools. In AVoCS 2010. Universität Düsseldorf, 2010.

[5]

M. Goldsmith, B. Roscoe, and P. Armstrong. Failures-Divergence Refinement - FDR2 User Manual. http://www.fsel.com/fdr2_manual.html, 2005.

[6]

Thomas Göthel and Sabine Glesner. An Approach for Machine-Assisted Verification of Timed CSP Specifications. Innovations in Systems and Software Engineering - A NASA Journal, 7, 2010.

Digital Library

[7]

C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall International, 1985.

Digital Library

[8]

Y. Isobe and M. Roggenbach. A Generic Theorem Prover of CSP Refinement. In Tools and Algorithms for the Construction and Analysis of Systems, pages 108--123. Springer, 2005.

Digital Library

[9]

Szilárd Jaskó, Gyula Simon, Katalin Tarnay, Tibor Dulai, and Dániel Muhi. CSP-based modelling for self-adaptive applications. In Infocommunications Journal, volume LVIV, pages 14--21, 2009.

[10]

M. Kleine and B. Bartels. On Using CSP for the Construction of Concurrent Programs. In International Conference on Software Engineering Theory and Practice (SETP-10), Orlando, Florida, USA, July 2010.

[11]

M. Kleine, B. Bartels, T. Göthel, and S. Glesner. Verifying the Implementation of an Operating System Scheduler. In 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE '09), pages 285--286, Tianjin, China, July 2009. IEEE Computer Society Press.

Digital Library

[12]

M. Kleine, B. Bartels, T. Göthel, S. Helke, and D. Prenzel. LLVM2CSP: Extracting CSP Models from Concurrent Programs. In Third NASA Formal Methods Symposium, 2011. to appear.

Digital Library

[13]

M. Kleine and S. Helke. Low Level Code Verification Based on CSP Models. In M. Oliveira and J. Woodcock, editors, Brazilian Symposium on Formal Methods (SBMF 2009), pages 266--281. Springer, August 2009.

Digital Library

[14]

Anna Kosek, Aly Syed, Jon Kerridge, and Alistair Armitage. A dynamic connection capability for pervasive adaptive environments using jcsp, 2009.

[15]

C. Lattner and V. Adve. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04), pages 75--85, Palo Alto, California, Mar 2004. IEEE Computer Society.

Digital Library

[16]

M. Leuschel and M. Fontaine. Probing the Depths of CSP-M: A new FDR-compliant Validation Tool. In International Conference on Formal Engineering Methods, pages 278--297. Springer, 2008.

Digital Library

[17]

M. Leuschel, T. Massart, and A. Currie. How to make FDR Spin: LTL model checking of CSP using Refinement. In P. Zave J. N. Oliviera, editor, FME 2001: Formal Methods for Increasing Software Productivity. Springer-Verlag, March 2001.

Digital Library

[18]

Gavin Lowe. Specification of communicating processes: temporal logic versus refusals-based refinement. Form. Asp. Comput., 20(3):277--294, 2008.

[19]

Jeff Magee and Jeff Kramer. Dynamic structure in software architectures. In In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, 1996.

Digital Library

[20]

S. Montenegro, K. Briess, and H. Kayal. Dependable Software (BOSS) for the BEESAT Pico Satellite. In DASIA 2006, Data Systems In Aerospace - DASIA 2006, May 2006, Berlin. ESTEC, 2006.

[21]

T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

Digital Library

[22]

D. Plagge and M. Leuschel. Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more. STTT, 2008.

Digital Library

[23]

A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 2005.

Digital Library

[24]

A.W. Roscoe. Csp is expressive enough for pi. to appear in Reflections on the work of C. A. R. Hoare, 2010. Springer.

Digital Library

[25]

Klaus Schneider, Tobias Schuele, and Mario Trapp. Verifying the adaptation behavior of embedded systems. In Proceedings of the 2006 international workshop on Self-adaptation and self-managing systems, SEAMS '06, pages 16--22, New York, NY, USA, 2006. ACM.

Digital Library

[26]

P. H. Welch. Java Threads in the Light of occam/CSP. In P. H. Welch and A. W. P. Bakkers, editors, Architectures, Languages and Patterns for Parallel and Distributed Applications, volume 52 of Concurrent Systems Engineering Series, pages 259--284, Amsterdam, April 1998. WoTUG, IOS Press.

[27]

P. T. Welch, F. R. M. Barnes, and F. A. C. Polack. Communicating complex systems. In 11th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2006), page 11 pp. 0-0 2006.

Digital Library

Cited By

Sun CGong YLi MXu LHan JHan Y(2024)Detecting Inconsistencies in Microservice-Based Systems: An Annotation-Assisted Scenario-Oriented ApproachIEEE Transactions on Services Computing10.1109/TSC.2024.339965217:5(2194-2209)Online publication date: Sep-2024
https://doi.org/10.1109/TSC.2024.3399652
Kachi FBouanaka C(2023)A hybrid model for efficient decision-making in self-adaptive systemsInformation and Software Technology10.1016/j.infsof.2022.107063153:COnline publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1016/j.infsof.2022.107063
Graics BMolnár VMajzik I(2023)Component‐based specification, design and verification of adaptive systemsSystems Engineering10.1002/sys.2167526:5(567-589)Online publication date: 6-Apr-2023
https://doi.org/10.1002/sys.21675
Show More Cited By

Index Terms

A CSP-based framework for the specification, verification, and implementation of adaptive systems
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

Recommendations

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
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 ...
Modular verification of dynamically adaptive systems
AOSD '09: Proceedings of the 8th ACM international conference on Aspect-oriented software development

Cyber-physical systems increasingly rely on dynamically adaptive programs to respond to changes in their physical environment; examples include ecosystem monitoring and disaster relief systems. These systems are considered high-assurance since errors ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SEAMS '11: Proceedings of the 6th International Symposium on Software Engineering for Adaptive and Self-Managing Systems

May 2011

246 pages

ISBN:9781450305754

DOI:10.1145/1988008

Program Chairs:
Holger Giese
Hasso Plattner Institute, Germany
,
Betty H.C. Cheng
Michigan State University, USA

Copyright © 2011 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 May 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICSE11

Sponsor:

SIGSOFT

ICSE11: International Conference on Software Engineering

May 23 - 24, 2011

HI, Waikiki, Honolulu, USA

Acceptance Rates

Overall Acceptance Rate 17 of 31 submissions, 55%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
465
Total Downloads

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

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sun CGong YLi MXu LHan JHan Y(2024)Detecting Inconsistencies in Microservice-Based Systems: An Annotation-Assisted Scenario-Oriented ApproachIEEE Transactions on Services Computing10.1109/TSC.2024.339965217:5(2194-2209)Online publication date: Sep-2024
https://doi.org/10.1109/TSC.2024.3399652
Kachi FBouanaka C(2023)A hybrid model for efficient decision-making in self-adaptive systemsInformation and Software Technology10.1016/j.infsof.2022.107063153:COnline publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1016/j.infsof.2022.107063
Graics BMolnár VMajzik I(2023)Component‐based specification, design and verification of adaptive systemsSystems Engineering10.1002/sys.2167526:5(567-589)Online publication date: 6-Apr-2023
https://doi.org/10.1002/sys.21675
Ye XLiu WWang N(2021)Runtime Verification of Multi-Agent Self-Adaptive System2021 IEEE 24th International Conference on Computer Supported Cooperative Work in Design (CSCWD)10.1109/CSCWD49262.2021.9437643(12-17)Online publication date: 5-May-2021
https://doi.org/10.1109/CSCWD49262.2021.9437643
Camilli MCapra L(2021)Formal specification and verification of decentralized self-adaptive systems using symmetric netsDiscrete Event Dynamic Systems10.1007/s10626-021-00343-331:4(609-657)Online publication date: 1-Dec-2021
https://dl.acm.org/doi/10.1007/s10626-021-00343-3
Jarrar AAit Wakrime ABalouki Y(2020)Formal approach to model complex adaptive computing systemsComplex Adaptive Systems Modeling10.1186/s40294-020-0069-78:1Online publication date: 12-Feb-2020
https://doi.org/10.1186/s40294-020-0069-7
Heinzemann CBecker SVolk A(2019)Transactional execution of hierarchical reconfigurations in cyber-physical systemsSoftware and Systems Modeling (SoSyM)10.1007/s10270-017-0583-z18:1(157-189)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10270-017-0583-z
Camilli MBellettini CCapra LPérez JMirandola RChen H(2018)A high-level petri net-based formal model of distributed self-adaptive systemsProceedings of the 12th European Conference on Software Architecture: Companion Proceedings10.1145/3241403.3241445(1-7)Online publication date: 24-Sep-2018
https://dl.acm.org/doi/10.1145/3241403.3241445
Borda APasquale LKoutavas VNuseibeh BAndersson JWeyns D(2018)Compositional verification of self-adaptive cyber-physical systemsProceedings of the 13th International Conference on Software Engineering for Adaptive and Self-Managing Systems10.1145/3194133.3194146(1-11)Online publication date: 28-May-2018
https://dl.acm.org/doi/10.1145/3194133.3194146
Borda AKoutavas VGnesi SPlat NSpoletini PPelliccione P(2018)Self-adaptive automataProceedings of the 6th Conference on Formal Methods in Software Engineering10.1145/3193992.3194001(64-73)Online publication date: 2-Jun-2018
https://dl.acm.org/doi/10.1145/3193992.3194001
Show More Cited By

View Options

Get Access

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents