"Nen\u00ED k dispozici"@cs . "Waszniowski, Libor" . . . . "5"^^ . "Formal Verification of OSEK/VDX Based Applications"@en . "Formal Verification of OSEK/VDX Based Applications" . . "21230" . "RIV/68407700:21230/04:03102811!RIV/2005/AV0/212305/N" . "[F58F0CF544B5]" . "This article shows, how a preemptive multitasking application running under a real-time operating system compliant with OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several tasks, it includes synchronization by events and resource sharing. For such system, model-checking theory based on timed automata and implemented in model-checking tools can be used to verify time and logical properties of the proposed model. It is shown that the proposed model is over-approximation in the case of preemptive scheduling policy."@en . . . . . "P(1ET400750406)" . "RIV/68407700:21230/04:03102811" . . "2"^^ . . . . "Formal Verification of OSEK/VDX Based Applications"@en . "Hanz\u00E1lek, Zden\u011Bk" . . . "Lisabon" . "University of Lisbon" . "2"^^ . "564700" . . "This article shows, how a preemptive multitasking application running under a real-time operating system compliant with OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several tasks, it includes synchronization by events and resource sharing. For such system, model-checking theory based on timed automata and implemented in model-checking tools can be used to verify time and logical properties of the proposed model. It is shown that the proposed model is over-approximation in the case of preemptive scheduling policy." . "Nen\u00ED k dispozici"@cs . "Nen\u00ED k dispozici"@cs . "Real-time"@en . "2004-12-05+01:00"^^ . "Formal Verification of OSEK/VDX Based Applications" . "60 ; 64" . "Lisboa" . "RTSS 2004 Work-In-Progress Proceedings" .