• DocumentCode
    3142439
  • Title

    Developing reactive systems in a VDM framework

  • Author

    Ledru, Y.

  • Author_Institution
    Unite d´´Inf., Univ. Catholique de Louvain, Louvain-La-Neuve, Belgium
  • fYear
    1991
  • fDate
    25-26 Oct 1991
  • Firstpage
    130
  • Lastpage
    139
  • Abstract
    The detailed validation of reactive systems, using an extension of VDM, is studied. The specification and proof of behavioural aspects is added to VDM by using traces of the input/output activities. The major objective of the work is to progress in the comprehension of the practical implications of the specification, design, and symbolic validation of machine-checked reactive systems
  • Keywords
    Vienna development method; formal specification; program verification; VDM framework; behavioural aspects; detailed validation; input/output activities; machine-checked reactive systems; practical implications; symbolic validation; Explosions; Formal specifications; Protocols; Software systems;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Software Specification and Design, 1991., Proceedings of the Sixth International Workshop on
  • Conference_Location
    Como
  • Print_ISBN
    0-8186-2320-9
  • Type

    conf

  • DOI
    10.1109/IWSSD.1991.213068
  • Filename
    213068