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

-- Gunter Mussbacher - 12 Oct 2005

Discussion

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