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.
Chapter PDF
Similar content being viewed by others
Keywords
References
Amyot, D. (1994) Formalization of Timethreads Using LOTOS. M.Sc. Thesis, Dept. of Computer Science, University of Ottawa, Ottawa, Canada.
Bolognesi, T. (1990) “A Graphical Composition Theorem for Networks of LOTOS Processes”. In: Proceedings of the 10th International Conference on Distributed Computing Systems, IEEE Computer Society Press, 88–95.
Bordeleau, F. (1993) Visual Descriptions, Formalisms and the Design Process. M.Sc. Thesis, School of Computer Science, TR-SCE-93–35, Carleton University, Ottawa, Canada.
Bordeleau, E and Amyot, D. (1993) “LOTOS Interpretation of Timethreads: A Method and a Case Study”. TR-SCE-93–34, Dept. of Systems and Computer Engineering, Carleton University, Ottawa, Canada
Bordeleau, E and Locas, M. (1994) “Timethread-Centered Design Process: A Study on Transformation Techniques and a Telephone System Case Study”. TR-SCE-94–18, Dept. of Systems and Computer Engineering, Carleton University, Ottawa, Canada.
Brinksma, E. and Eertink, H. (1993) “Goal-Driven LOTOS Execution”. In: A. Danthine, G. Leduc, and P. Wolper (Eds), Protocol Specification, Testing and Verification, XIII, North-Holland, 45–60.
Buhr, R.J.A. and Casselman, R.S. (1995) Use Case Maps for Object-Oriented Systems, Prentice-Hall, USA. To appear in October.
Buhr, R.J.A. and Casselman, R.S. (1992) “Architectures with Pictures”. In: Proceedings of OOPSLA’92, ACM/SIGPLAN, Vancouver, Canada, 466–483.
Clarke, E.M., Emerson, E.A. and A.P. Sistla (1986) “Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications”. ACM TOPLAS, 8 (2), 244–263.
de Frutos-Eserig, D. (1993) “A Characterization of LOTOS Representable Networks of Parallel Processes”. In: R Scollo (Ed), Proceedings of AMAST’93.
Ghribi, B. (1992) A Model Checker For LOTOS. M.Sc. Thesis, Dept. of Computer Science, University of Ottawa, Ottawa, Canada.
Ghribi, B. and Logrippo, L. (1993) “A Validation Environment for LOTOS”. In: A. Danthine, G. Leduc, and P. Wolper (Eds), Protocol Specification, Testing and Verification XIII, North-Holland.
Haj-Hussein, M., Logrippo, L. and Sincennes, J. (1993) “Goal Oriented Execution for LOTOS”. In: M. Diaz and R. Groz (Eds), Formal Description Techniques V, North-Holland, 311–327.
Hinterplattner, J., Nirshl, H. and Saria H. (1991), “Process Topology Diagram”, In: J. Quemada, J. Manas, and E. Vizquez (Eds), Formal Description TechniquesIII, North-Holland.
ISO (1988), Information Processing Systems, Open Systems Interconnection, “LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour”, IS 8807.
Quemada, J., Pavón, S. and Fernandez, A. (1988) “Transforming LOTOS Specifications with LOLA: The Parametrized Expansion”. In: K. J. Turner (Ed), Formal Description TechniquesI, IFIP/North-Holland, 45–54.
Vigder, M. and Buhr, R.J.A. (1992) “Using LOTOS in a Design Environment”. In: K.R.Parker, G.A. Rose, (Eds), Formal Description Techniques, IV, IFIP/North-Holland, 1–14.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Amyot, D., Bordeleau, F., Buhr, R.J.A., Logrippo, L. (1996). Formal support for design techniques: a Timethreads-LOTOS approach. In: Bochmann, G.v., Dssouli, R., Rafiq, O. (eds) Formal Description Techniques VIII. FORTE 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34945-9_5
Download citation
DOI: https://doi.org/10.1007/978-0-387-34945-9_5
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2958-9
Online ISBN: 978-0-387-34945-9
eBook Packages: Springer Book Archive