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 |
| _version_ | 1819180228387274752 |
|---|---|
| author | Liviu Haţegan Piroska Haller |
| author_facet | Liviu Haţegan Piroska Haller |
| author_sort | Liviu Haţegan |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-22T22:11:00Z |
| format | Article |
| id | doaj.art-b46c608024304c15a2b8d03ede762089 |
| institution | Directory Open Access Journal |
| issn | 1841-9267 2285-438X |
| language | English |
| last_indexed | 2024-12-22T22:11:00Z |
| publishDate | 2009-12-01 |
| publisher | Editura Universităţii "Petru Maior" |
| record_format | Article |
| series | Scientific Bulletin of the ''Petru Maior" University of Tîrgu Mureș |
| spelling | doaj.art-b46c608024304c15a2b8d03ede7620892022-12-21T18:10:53ZengEditura Universităţii "Petru Maior"Scientific Bulletin of the ''Petru Maior" University of Tîrgu Mureș1841-92672285-438X2009-12-016 (XXIII)22127Formal Verification and Implementation of Real-Time ApplicationsLiviu HaţeganPiroska HallerThis 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.http://scientificbulletin.upm.ro/papers/2010/12/Formal-Verification-and-Implementation-of-Real-Time-Applicat.pdfembedded real-time multitasking applicationscooperative scheduler modelpre-emptive application tasks |
| spellingShingle | Liviu Haţegan Piroska Haller Formal Verification and Implementation of Real-Time Applications Scientific Bulletin of the ''Petru Maior" University of Tîrgu Mureș embedded real-time multitasking applications cooperative scheduler model pre-emptive application tasks |
| title | Formal Verification and Implementation of Real-Time Applications |
| title_full | Formal Verification and Implementation of Real-Time Applications |
| title_fullStr | Formal Verification and Implementation of Real-Time Applications |
| title_full_unstemmed | Formal Verification and Implementation of Real-Time Applications |
| title_short | Formal Verification and Implementation of Real-Time Applications |
| title_sort | formal verification and implementation of real time applications |
| topic | embedded real-time multitasking applications cooperative scheduler model pre-emptive application tasks |
| url | http://scientificbulletin.upm.ro/papers/2010/12/Formal-Verification-and-Implementation-of-Real-Time-Applicat.pdf |
| work_keys_str_mv | AT liviuhategan formalverificationandimplementationofrealtimeapplications AT piroskahaller formalverificationandimplementationofrealtimeapplications |