| products/sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: VDMOriginal von: VDM© |
|
||||||
|
system RadNavSys
instance variables -- create application tasks static public mmi : MMI := new MMI(); static public radio : Radio := new Radio(); static public navigation : Navigation := new Navigation(); -- create CPUs (policy, capacity) CPU1 : CPU := new CPU (<FP>, 22E6); CPU2 : CPU := new CPU (<FP>, 11E6); CPU3 : CPU := new CPU (<FP>, 113E6); -- create a bus (policy, capacity, topology) BUS1 : BUS := new BUS (<CSMACD>, 72E3, {CPU1, CPU2, CPU3}) operations public RadNavSys: () ==> RadNavSys RadNavSys () == ( -- deploy mmi on CPU1 CPU1.deploy(mmi,"MMIT"); CPU1.setPriority(MMI`HandleKeyPress,100); CPU1.setPriority(MMI`UpdateScreen,90); -- deploy radio on CPU2 CPU2.deploy(radio,"RadioT"); CPU2.setPriority(Radio`AdjustVolumeUp,100); CPU2.setPriority(Radio`AdjustVolumeDown,100); CPU2.setPriority(Radio`HandleTMC,90); -- deploy navigation on CPU3 CPU3.deploy(navigation,"NavT"); CPU3.setPriority(Navigation`DatabaseLookup, 100); CPU3.setPriority(Navigation`DecodeTMC, 90) -- starting the CPUs and BUS is implicit ); /* timing invariants separate(#fin(MMI`UpdateScreen), #fin(MMI`UpdateScreen), 500 ms); */ end RadNavSys ¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
