uppaaltutorial (Uppaal - описание), страница 7

Ideally, amodel should not just describe the specific system at hand: by appropriate instantiation and dimensioning it should be possible to model a whole class of similarsystems.Our jobshop model can be extended or reused in several ways: we can easily increase the number of jobbers and tools, modify the sequence of jobs, and modifythe timing parameters. What can not be changed so easily are the assumptions onwhich tools can be used for which jobs. The next chapter presents a more genericversion of the jobshop model in which variations of these assumptions can betrivially modified. However, this requires the use of some advanced modellingfeatures, which are explained in the next chapter.7.

A good model has been designed and encoded for interoperability and sharingof semantics. Model-driven development of an embedded system typically leadsto a plethora of models, all presenting different views on and abstractions ofthe system. If a model is not somehow linked to other models, its usefulnesswill be limited. Ideally therefore, the relationships between all models should beproperly defined, for instance via formal refinement relations.In this chapter, we have not addressed issues of interoperability and sharing.

Werefer to chapters XX and YY add refs of this handbook for a description ofvarious links between Uppaal and other model based development tools. In amore realistic version of the jobshop example, in which for instance the jobbersare replaced by robots, one of the things one could do is to take the schedulescomputed by Uppaal and translate these to control programs for the robots. Suchan approach (using Uppaal) is described for instance in [7]. (and Chapter XX?)Clearly, there are many relationships and dependencies between the criteria. If amodel is traceable, that is, links between the structural elements of the model andthe aspects of the object of modelling are clearly documented, then chances increasethat the model will be truthful.

Also, if a model has been set up in a modular way,then one may apply a divide-and-conquer strategy both for establishing truthfulnessof the model and for analysis.biosection??References1. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, Cambridge, Massachusetts, 2008.2. G. Behrmann, A. David, and K.G. Larsen. A tutorial on Uppaal.

In M. Bernardo and F. Corradini, editors, Formal Methods for the Design of Real-Time Systems, International School onFormal Methods for the Design of Computer, Communication and Software Systems, SFMRT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures, volume 3185 of LectureNotes in Computer Science, pages 200–236. Springer, 2004.3. E.M. Clarke, O. Grumberg, and D. Peled.

Model Checking. MIT Press, Cambridge, Massachusetts, 1999.1 A First Introduction to Uppaal314. W.H.J. Feijen, Gasteren A.J.M. van, D. Gries, and J. Misra, editors. Beauty is our business— A Birthday Salute to Edsger W. Dijkstra, Texts and Monographs in Computer Science.Springer-Verlag, 1990.5. O. Grumberg and H. Veith, editors. 25 Years of Model Checking: History, Achievements,Perspectives, volume 5000 of Lecture Notes in Computer Science. Springer, 2008.6. C.A.R.

Hoare. Communicating Sequential Processes. Prentice-Hall International, EnglewoodCliffs, 1985.7. T. Hune, K.G. Larsen, and P. Pettersson. Guided synthesis of control programs using Uppaal.Nord. J. Comput., 8(1):43–64, 2001.8. C.A.J. Hurkens. Spreading gossip efficiently. Nieuw Archief voor Wiskunde, 5/1(2):208–210,June 2000.9. A. Mader, H. Wupper, and M. Boon. The construction of verification models for embeddedsystems. Technical Report TR-CTIT-07-02, Centre for Telematics and Information Technology, University of Twente, The Netherlands, 2007.10.

R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs,1989.11. Wikipedia. List of model checking tools, February 2011. http://en.wikipedia.org/wiki/List_of_model_checking_tools..