TRoS: formal specification and verification for platform-constrained embedded software

다국어 초록 (Multilingual Abstract)

This thesis presents a formal analysis framework for the development of real-time embedded software. In our framework, the application software and the real-time platform, i.e. real-time operating system, are formally and individually defined in their appropriate specification language. For the analysis, behavioral models for the embedded software components are analyzed independently in respect of their own characteristics, and then they are composed into one execution system to analyze their composite behavior in their interaction.

The real-time embedded software often consists of application software and platform software, i.e. real-time operating system. The two embedded software components continuously interact with one another to achieve the purpose of the system; the application software calls a real-time operating system for system services, and the real-time operating system manages each process of application software to fairly share a limit resource. Thus, they are heterogeneous in a sense that application software is oriented to data-flow for the user's functionalities, whereas the platform is oriented to control-flow for control of software's executions. Hence, it is not easy to represent those capabilities in one behavioral model to analyze their composite behaviors.

For the modeling of application software and platform, we propose here the use of Statecharts and its extension, named TRoS (Timed and Resource-oriented Statecharts), to formally specify respectively a functional behavior and a timed and resource-constrained behavior of application software, in particular, the use of ACSR (Algebra of Communicating and Shared Resources) to formally specify a controlling behavior of real-time operating system. TRoS we formally define here is an extension of Statecharts in terms of time and resource constraints for real-time embedded system. It has the capability to be extended from Statecharts only by annotation rules we define here. For analyzing the composite behavior of the two embedded software components, we present formal definition of composite behavior of application software and platform simulating their interactive behaviors. In particular, only the interaction behavior of TRoS is extracted from TRoS and abstracted into application software behavior model of ACSR, and the ACSR model is composed with ACSR model of platform, to prove the correctness and consistency of their interactive behaviors.

Using our analysis framework, 1) the standard platform, such as ARINC 653 and OSEK, can be formalized into a formal specification in terms of a controlling behavior for application software, 2) application software behavior in Statecharts can be transformed into TRoS to represent a timed and resource-constrained functional behavior of the software, and 3) the timed and resource-constrained behavior of application software and the controlling behavior of platform software, i.e, real-time operating system, can be incorporated into a behavior system to analyze the correctness and consistency of their parallel behavior in their interaction.

In this thesis, we apply our framework to the development of avionics embedded application software to run on a standard real-time platform, ARINC 653, to illustrate our approach to the analysis of real-time embedded software. Moreover, our approach using TRoS and ACSR is shown to be feasible, being applied to MDA (Model-Driven Architecture) which emphasizes model transformation and analysis from high-level abstraction and low-level abstraction of embedded software.

목차 (Table of Contents)

• 1 Introduction . . . 1
• 2 Related Works . . . 7
• 3 Formal Specifcations for Real-time Embedded Software . . . . . . .9
• 3.1 ACSR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
• 3.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
• 3.1.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
• 3.2 Statecharts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
• 3.2.1 Use of Statecharts . . . . . . . . . . . . . . . . . . . . . . . . 22
• 3.2.2 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
• 3.2.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
• 3.2.4 Timed Behavior of Statecharts . . . . . . . . . . . . . . . . . 29
• 4 Timed and Resource-oriented Statecharts 32
• 4.1 Related Works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
• 4.2 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
• 4.3 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
• 4.4 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
• 4.5 Process-level Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 49
• 4.6 Transformation of TRoS from Statecharts . . . . . . . . . . . . . . . 51
• 5 Composite Behaviors of TRoS
• ACSR 58
• 5.1 TRoS
• ACSR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
• 5.2 Specification of Real-Time Embedded Software System using TRoS
• ACSR . . 65
• 5.2.1 RTOS Service Models in ACSR . . . . . . . . . . . . . . . . . 65
• 5.2.2 Application Software Models in TRoS . . . . . . . . . . . . . 68
• 5.2.3 Embedded Software Models . . . . . . . . . . . . . . . . . . . 70
• 5.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
• 6 Case Study:
• Formal Specifcation and Verifcaiton of ARINC 653-based Real-Time Embedded Software .74
• 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
• 6.2 Platform-based Development using TRoS
• ACSR . . . . . . . . . . 76
• 6.3 ARINC 653 Service (APEX) Overview . . . . . . . . . . . . . . . . . 78
• 6.4 ARINC Process . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
• 6.5 Modeling ARINC 653 Services in ACSR . . . . . . . . . . . . . . . . 84
• 6.6 Modeling an Avionics Application : ON FLIGHT . . . . . . . . . . . 87
• 6.6.1 Avionics Application Behavioral Models in Statecharts . . . . 90
• 6.6.2 Real-time Application Models in TRoS . . . . . . . . . . . . 93
• 6.6.3 ARINC 653-based Real-time Embedded Software Models . . 100
• 6.7 Verification of ARINC 653-based Real-time Embedded Software . . . 103
• 6.8 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
• 7 Case Study: Mode-Driven Architecture based on TRoS and ACSR . . .114
• 7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
• 7.2 Related Works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
• 7.3 Our Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
• 7.3.1 Modeling Behaviors of PIM and PSM . . . . . . . . . . . . . 119
• 7.3.2 Analysis for MDA Behavior Models . . . . . . . . . . . . . . 121
• 7.3.3 Discussion for our MDA Behavior Models . . . . . . . . . . . 122
• 7.4 Case Study: Distance Control Module of Railway Interlocking Control
• System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
• 7.4.1 DCM Models . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
• 7.4.2 PSM Behavior Models . . . . . . . . . . . . . . . . . . . . . . 127
• 7.4.3 Analysis for DCM . . . . . . . . . . . . . . . . . . . . . . . . 129
• 7.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
• 8 Conclusions . . . 133
• Appendices . . . 135
• A Formal Behavior Models of ON FLIGHT based on ARINC 653 . . . 136
• B Formal Specication of ARINC 653-based System Services in ACSR . . . 148
• B.1 Buffer Service . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148
• B.2 Blackboard Service . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
• B.3 Semaphore Service . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160
• B.4 Event Service . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
• C Formal Specication of DCM and uC/OS System Services in ACSR . . . . . . . .171
• C.1 uC/OS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172
• C.2 DCM
• uC/OS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176
• References . . . 190