Formal Verification and Implementation of Real-Time Applications
This paper presents a method for the formal description, verification and automatic source code generation of embedded real-time multitasking applications, based on a model consisting of networks of timed automata. The model describes a real-time operating system kernel and application tasks, taking...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Editura Universităţii "Petru Maior"
2009-12-01
|
| Series: | Scientific Bulletin of the ''Petru Maior" University of Tîrgu Mureș |
| Subjects: | |
| Online Access: | http://scientificbulletin.upm.ro/papers/2010/12/Formal-Verification-and-Implementation-of-Real-Time-Applicat.pdf |
| Summary: | This paper presents a method for the formal description, verification and automatic source code generation of embedded real-time multitasking applications, based on a model consisting of networks of timed automata. The model describes a real-time operating system kernel and application tasks, taking into consideration both non-preemptive and preemptive scheduling. The timing properties of theproposed model can be verified using a modelchecking tool. We also provide a solution for C source code generation based on the application’s model. For this purpose a unified resource access interface was implemented. |
|---|---|
| ISSN: | 1841-9267 2285-438X |