TY - CHAP
T1 - Formal modeling for a real-time scheduler and schedulability analysis
AU - Kim, Sung Jae
AU - Choi, Jin Young
PY - 2003
Y1 - 2003
N2 - The reliability of safety-critical embedded real-time system depends partly on that of the system design. Because of this, formal methods have been adopted in the design phase of developing such systems, and various kinds of formal methods have been introduced and used in practice. Many successful results have been published in application systems/softwares. However, studies on formal specification for embedded kernel, like scheduler, are relatively few due to the complexity of the software. In this paper, we present a formal specification for real-time scheduler based on SyncCharts. We specify a scheduler of which policies are rate monotonic, as well as Priority Ceiling Protocol, and perform schedulability analysis by formal verification. Once requirements of the real-time scheduler and timing properties of given tasks are satisfied, a real code can be automatically generated and, we believe, ported in a real target platform.
AB - The reliability of safety-critical embedded real-time system depends partly on that of the system design. Because of this, formal methods have been adopted in the design phase of developing such systems, and various kinds of formal methods have been introduced and used in practice. Many successful results have been published in application systems/softwares. However, studies on formal specification for embedded kernel, like scheduler, are relatively few due to the complexity of the software. In this paper, we present a formal specification for real-time scheduler based on SyncCharts. We specify a scheduler of which policies are rate monotonic, as well as Priority Ceiling Protocol, and perform schedulability analysis by formal verification. Once requirements of the real-time scheduler and timing properties of given tasks are satisfied, a real code can be automatically generated and, we believe, ported in a real target platform.
UR - http://www.scopus.com/inward/record.url?scp=35248836153&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35248836153&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-45145-7_23
DO - 10.1007/978-3-540-45145-7_23
M3 - Chapter
AN - SCOPUS:35248836153
SN - 3540406735
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 253
EP - 258
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Malyshkin, Victor
PB - Springer Verlag
ER -