Abstract

A design methodology which allies the graphical expressiveness of the timethread notation with the analytical power of the LOTOS language and its associated tools is presented. The concept of timethread is at the basis of a design methodology based on scenarios. A simple telephone system is used as an example. It is shown how the main scenarios of such a system can be expressed by the timethread notation, leading to an abstract system design. Further, it is shown how the notation can be translated into LOTOS. LOTOS tools are used to validate the high-level design. Tools used include LOLA for analysis and design testing, LMC for checking temporal logic properties, and GOAL for checking reachability of actions.

HTML version of paper available at http://www.csi.uottawa.ca/~damyot/phd/forte95/forte95.html

-- GunterMussbacher - 12 Oct 2005

Discussion

  • Please feel free to discuss this article directly on this page. Constructive comments are welcomed! Please sign your TWiki name.

FormForVirtualLibrary edit

Title Formal support for design techniques: a Timethreads-LOTOS approach
Authors D. Amyot, F. Bordeleau, R.J.A. Buhr, and L. Logrippo
Type Conference
Conference/Journal Title FORTE VIII, 8th International Conference on Formal Description Techniques
Volume/Number
Editors
Publisher Chapman & Hall
Month October
Year 1995
Pages 57-72
Keywords FDT-based software engineering, tools and tool support, design and design validation, timethreads, LOTOS
Topic attachments
I Attachment Action Size Date Who Comment
forte95.pdfpdf forte95.pdf manage 210 K 12 Oct 2005 - 19:07 GunterMussbacher Forte95 paper
Topic revision: r1 - 12 Oct 2005, GunterMussbacher
This site is powered by FoswikiCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding Foswiki? Send feedback