Skip to main content
SpringerLink
Log in

Invariant-Based Synthesis of Fault-Tolerant Systems

  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1926))

Abstract

Statecharts are a very widely used formalism for reactive system development, however there are problems in using them as a fully formal specification notation because of the conflicting variants of statechart semantics which exist. In this paper a modular subset of statechart notation is defined which has a simple semantics, and permits compositional development and verification. Techniques for decomposing specifications in this notation, design strategies for incorporating fault tolerance, and translation to the B formal language, are also described, and illustrated with extracts from a case study of a fault tolerant system.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Ali, B Specification of Steam Boiler, MSc thesis, Dept. of Computing, Imperial College, 1998.

    Google Scholar 

  2. K. Androutsopoulos. The Reactive System Design Tool, ROOS Project report, Department of Computing, Imperial College, 1999.

    Google Scholar 

  3. I. Hayes, A Survey of Data Refinement and Full Abstraction in VDM and Z, Dept. of Computer Science, University of Queensland, 1991.

    Google Scholar 

  4. International Electrotechnical Commission, IEC 61508: Functional Safety of Electrical/Electronic/Programmable Electronic Safety-Related Systems, 1999.

    Google Scholar 

  5. K. Lano, J. Bicarregui, and A. Evans. Structured Axiomatic Semantics for UML Models, ROOM 2000 Proceedings, to appear in Electronic Workshops in Computer Science, Springer-Verlag, 2000.

    Google Scholar 

  6. K. Lano, K. Androutsopoulos, D. Clark, Structuring and Design of Reactive Systems using RSDS and B, FASE 2000, to appear in LNCS, Springer-Verlag, 2000.

    Google Scholar 

  7. C. Lewerentz, T. Lindner (eds.), Formal Development of Reactive Systems, LNCS Vol. 891, Springer-Verlag, 1995.

    MATH  Google Scholar 

  8. A. Lötzbeyer, R Mühlfeld, Task Description of a Flexible Production Cell with Real Time Properties, FZI, Karlsruhe, 1996.

    Google Scholar 

  9. F. Mejia, Formalising Existing Safety-Critical Software, FMERail Workshop No. 2, London, UK, 1998. http://www.ifad.dk/Projects/fmerail.htm.

  10. E. Sekerinski. Graphical Design of Reactive Systems. 2nd International Conference on B, Lecture Notes in Computer Science, Springer Verlag, pages 182–197, 1998.

    Google Scholar 

  11. H. Treharne, S. Schneider, Using a Process Algebra to Control B Operations, IFM’ 99, Springer-Verlag, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, King’s College London, Strand, WC2R 2LS, London

    K. Lano, K. Androutsopoulos & P. Kan

  2. Department of Computing, Imperial College, SW7 2BZ, London

    David Clark

Authors
  1. K. Lano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Clark
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. K. Androutsopoulos
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. P. Kan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Tata Research Development and Design Centre, 54B, Hadapsar Industrial Estate, Pune, 411013, India

    Mathai Joseph

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lano, K., Clark, D., Androutsopoulos, K., Kan, P. (2000). Invariant-Based Synthesis of Fault-Tolerant Systems. In: Joseph, M. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2000. Lecture Notes in Computer Science, vol 1926. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45352-0_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-45352-0_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41055-3

  • Online ISBN: 978-3-540-45352-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation