|
Author: Hugo Macedo
This model is made by Hugo Macedo as a part of his MSc thesis of a
pacemaker according to the grand challenge provided by Boston
Scientific in this area. This is the last of a series of VDM models
of the pacemaker and it incorporates a number of modes for the
pacemaker. More information can be found in:
Hugo Macedo, Validating and Understanding Boston Scientific Pacemaker
Requirements, MSc thesis, Minho University, Portugal, October 2007.
Hugo Daniel Macedo, Peter Gorm Larsen and John Fitzgerald, Incremental
Development of a Distributed Real-Time Model of a Cardiac Pacing System
using VDM, In FM 2008: Formal Methods, 15th International Symposium on
Formal Methods, Eds, Jorge Cuellar and Tom Maibaum and Kaisa Sere, 2008,
Springer-Verlag, Lecture Notes in Computer Science 5014, pp. 181--197.
Language Version: vdm10
Entry point : new World("tests/scenarioGoodHeart.arg",<DOO>).Run()
Entry point : new World("tests/scenarioDoubleHeart.arg",<DOO>).Run()
Entry point : new World("tests/scenarioBrokenHeart.arg",<DOO>).Run()
Entry point : new World("tests/scenarioSometimesHeart.arg",<DOO>).Run()
Entry point : new World("tests/scenarioGoodHeart.arg",<AOO>).Run()
Entry point : new World("tests/scenarioDoubleHeart.arg",<AOO>).Run()
Entry point : new World("tests/scenarioBrokenHeart.arg",<AOO>).Run()
Entry point : new World("tests/scenarioSometimesHeart.arg",<AOO>).Run()
Entry point : new World("tests/scenarioGoodHeart.arg",<AAI>).Run()
Entry point : new World("tests/scenarioDoubleHeart.arg",<AAI>).Run()
Entry point : new World("tests/scenarioBrokenHeart.arg",<AAI>).Run()
Entry point : new World("tests/scenarioSometimesHeart.arg",<AAI>).Run()
Entry point : new World("tests/scenarioGoodHeart.arg",<DDD>).Run()
Entry point : new World("tests/scenarioDoubleHeart.arg",<DDD>).Run()
Entry point : new World("tests/scenarioBrokenHeart.arg",<DDD>).Run()
Entry point : new World("tests/scenarioSometimesHeart.arg",<DDD>).Run()
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
