loading...
Automating Checking of Models Built Using a Graphically Based Formal Modelling Language
Dallas, Texas November 03-November 06
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CMPSAC.2003.124532727th Annual International Computer So ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Robert John Walters, University of Southampton, UK
RDT is a graphical formal modelling language in which the modeller works by constructing diagrams of the processes in their model which they then join together to form complete systems. Aside from the benefits which accrue as a side effect of building a formal model of a proposed system, these diagrammatic models can be useful as a means of communication between the development team and the users. However one of the greatest benefits of a formal model is that it can be subjected to rigorous examination to ensure that it satisfies properties required of the system.
This paper describes the transformation used by the RDT toolset to generate Promela code (the input language of the SPIN model-checker) automatically from a model.
Citation:
Robert John Walters, "Automating Checking of Models Built Using a Graphically Based Formal Modelling Language," compsac, pp.98, 27th Annual International Computer Software and Applications Conference, 2003
Usage of this product signifies your acceptance of the Terms of Use.