Skip to main content
SpringerLink
Log in

Compositional Verification of Synchronous Networks

  • 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

We present a logical framework for the verification of synchronous networks in an assert-commit style. It is based on the known observation that the Hoare rule for sequential composition is sound and complete for parallel composition as well. The calculus we develop inside the framework is extremely simple, based on just one propositional tautology. Nevertheless, it is powerful enough to analyze the common proof strategies (monolithic, forward and backward) applied in automated verification of such networks. This analysis leads to an incremental verification method, based on successive construction of the weakest preconditions, in which the backward proof is driven by the property being verified. In the case of finite synchronous networks this construction can be carried out via simple manipulations on circuits, and circuit optimizers can be used incrementally to simplify the complexity of such backward proofs. The method should hopefully be applicable in verification of software synchronous systems, since the current compilers for synchronous languages generate quite redundant circuits.

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. Abadi, L. Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems, 15(1):73–132, Jan. 1993.

    Article  Google Scholar 

  2. M. Abadi, L. Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems, 17(3):507–534, May 1995.

    Article  Google Scholar 

  3. M. Abadi, G.D. Plotkin, A logical view of composition. Theoretical Computer Science, 114(1):3–30, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  4. H.R. Andersen, Partial Model Checking, Proceedings of LICS’95, IEEE Computer Society Press, 398–407, June 1995.

    Google Scholar 

  5. A. Aziz, F. Balarin, R. Brayton and A. Sangiovanni-Vincentelli, Sequential synthesis using S1S, Int. Conf. on Computer-Aided Design ICCAD’95, 1995.

    Google Scholar 

  6. G. Benveniste and P. Le Guernic, Synchronous programming with events and relations: the Signal language and its semantics, Science of Computer Programming, 16:103–149, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  7. G. Berry and G. Gonthier, The synchronous programming language Esterel: design, semantics, implementation, Science of Computer Programming, 19:87–152, 1992.

    Article  MATH  Google Scholar 

  8. G. Berry, A hardware implementation of pure Esterel, Sadhana, Academy Proceedings in Engineering Sciencies, Indian Academy of Sciences, 17:95–130, 1992.

    Google Scholar 

  9. N. Halbwachs, Synchronous Programming of Reactive Systems, Kluwer Academic Publishers, Dordrecht, 1993.

    MATH  Google Scholar 

  10. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous data flow programming language Lustre, Proceedings of the IEEE, 79(9):1305–1321, Sep. 1991.

    Google Scholar 

  11. N. Halbwachs, J.-C. Fernandez and A. Bouajjanni, An executable temporal logic to express safety properties and its connection with the language Lustre, Sixth Int. Symp. on Lucid and Intensional Programming, ISLIP’93, Quebec, April 1993.

    Google Scholar 

  12. N. Halbwachs, F. Lagnier and P. Raymond, Synchronous observers and the verification of reactive systems, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST’93, Workshops in Computing, Springer, Twente, June 1993.

    Google Scholar 

  13. L. Lamport, The temporal logic of actions,ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.

    Article  Google Scholar 

  14. F. Maraninchi, Operational and compositional semantics of synchronous automaton compositions, CONCUR’92, LNCS 630, Springer-Verlag, 550–564, Aug. 1992.

    Chapter  Google Scholar 

  15. A. Poigné and L. Holenderski, On the Combination of Synchronous Languages, Int. Symp. on Compositionality, COMPOS’97, LNCS 1536, State-of-the-Art Survey, Springer, 490–514, Sep. 1997.

    Google Scholar 

  16. E. Sentovich, H. Toma, and G. Berry, Efficient Latch Optimization Using Incompatible Sets, Int. Digital Automation Conf. DAC’97, Anaheim, 1997.

    Google Scholar 

  17. H. Toma, E. Sentovich, and G. Berry, Latch Optimization in Circuits Generated from High-Level Descriptions, Int. Conf. on Computer-Aided Design ICCAD’96, 1996.

    Google Scholar 

  18. C. Stirling, A complete compositional modal proof system for a subset of CCS, LNCS 194, Springer-Verlag, 475–486, 1985.

    Google Scholar 

  19. T. Shiple, G. Berry, H. Touati, Constructive analysis of cyclic circuits, Int. Design and Testing Conf. IDTC’96, Paris, France, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computing Sci., Technical University of Eindhoven, PO Box 513, 5600 MB, Eindhoven, The Netherlands

    Leszek Holenderski

Authors
  1. Leszek Holenderski
    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

Holenderski, L. (2000). Compositional Verification of Synchronous Networks. 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_18

Download citation

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

  • 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