Title Page

Abstract

Contents

Chapter 1. Introduction 18

Chapter 2. Related Works 24

Chapter 3. Formal Specifications for Real-time Embedded Software 26

3.1. ACSR 26

3.1.1. Syntax 28

3.1.2. Semantics 29

3.2. Statecharts 35

3.2.1. Use of statecharts 39

3.2.2. Syntax 40

3.2.3. Semantics 42

3.2.4. Timed Behavior of Statecharts 46

Chapter 4. Timed and Resource-oriented Statecharts 49

4.1. Related Works 52

4.2. Overview 54

4.3. Syntax 57

4.4. Semantics 60

4.5. Process-level Semantics 66

4.6. Transformation of TRoS from Statecharts 68

Chapter 5. Composite Behaviors of TRoS∥ACSR 75

5.1. TRoS∥ACSR 78

5.2. Specification of Real-Time Embedded Software System using TRoS∥ACSR 82

5.2.1. RTOS Service Models in ACSR 82

5.2.2. Application Software Models in TRoS 85

5.2.3. Embedded Software Models 87

5.3. Conclusion 89

Chapter 6. Case Study: Formal Specification and Verification of ARINC 653-based Real-Time Embedded Software 91

6.1. Introduction 91

6.2. Platform-based Development using TRoS∥ACSR 93

6.3. ARINC 653 Service(APEX) Overview 95

6.4. ARINC Process 98

6.5. Modeling ARINC 653 Services in ACSR 101

6.6. Modeling an Avionics Application : ON_FLIGHT 104

6.6.1. Avionics Application Behavioral Models in Statecharts 107

6.6.2. Real-time Application Models in TRoS 110

6.6.3. ARINC 653-based Real-time Embedded Software Models 117

6.7. Verification of ARINC 653-based Real-time Embedded Software 120

6.8. Conclusions 130

Chapter 7. Case Study: Mode-Driven Architecture based on TRoS and ACSR 131

7.1. Introduction 131

7.2. Related Works 134

7.3. Our Approach 135

7.3.1. Modeling Behaviors of PIM and PSM 136

7.3.2. Analysis for MDA Behavior Models 138

7.3.3. Discussion for our MDA Behavior Models 139

7.4. Case Study: Distance Control Module of Railway Interlocking Control System 140

7.4.1. DCM Models 142

7.4.2. PSM Behavior Models 144

7.4.3. Analysis for DCM 146

7.5. Conclusions 148

Chapter 8. Conclusions 150

Appendices 153

Appendix A. Formal Behavior Models of ON_FLIGHT based on ARINC 653 153

Appendix B. Formal Specification of ARINC 653-based System Services in ACSR 165

B.1. Buffer Service 165

B.2. Blackboard Service 172

B.3. Semaphore Service 177

B.4. Event Service 182

Appendix C. Formal Specification of DCM and uC/OS System Services in ACSR 188

C.1. uC/OS 189

C.2. DCM∥uC/OS 193

References 207

Table 3.1. Comparison of STATEMATE and UML Statecharts 47

Table 3.2. Execution Algorithm for the Clock-Synchronous Semantics 48

Table 3.3. Execution Algorithm for the Clock-Asynchronous Semantics 48

Table 4.1. Comparison of semantics of TRoS and other Statecharts 74

Table 5.1. Non-Prioritized Relation of TRoS∥ACSR 81

Table 5.2. uCOS Specification in ACSR 86

Table 6.1. Blackboard Service in ACSR 113

Table 6.2. Refinement of Functional Requirements of Statatecharts 114

Table 6.3. Necessary Interaction Methods for POSITION_INDICATOR 115

Table 6.4. Refinement of Requirement Specification of Statecharts 116

Table 6.5. Specification of Usable Resources and Assumed Worst-Execution Time for Operations 118

Table 6.6. Ttansformation of a Timed Action Node into ACSR 122

Table 6.7. POSITION_INDICATOR in Textual ACSR 125

Table 6.8. ARINC 654 Buffer Service Specification in ACSR 126

Table 7.1. Time and Resource Constraints 144

Table A.1. POSITION_INDICATOR in ACSR 2 162

Table A.2. FUEL_INDICATOR in ACSR 2 163

Table A.3. PARAMETER_REFRESHER in ACSR 2 164

Table B.1. APEX Buffer Service in ACSR 169

Table B.2. APEX Buffer Service in ACSR (cont'd) 170

Table B.3. APEX Buffer Service in ACSR (cont'd) 171

Table B.4. APEX Blackboard Service in ACSR 175

Table B.5. APEX Blackboard Service in ACSR (cont'd) 176

Table B.6. APEX Semaphore Service in ACSR 180

Table B.7. APEX Semaphore Service in ACSR (cont'd) 181

Table B.8. APEX Event Service in ACSR 185

Table B.9. APEX Event Service in ACSR (cont'd) 186

Table B.10. APEX Event Service in ACSR (cont'd) 187

Table C.1. uC/OS System Service in ACSR 189

Table C.2. uC/OS System Service in ACSR (cont'd) 190

Table C.3. uC/OS System Service in ACSR (cont'd) 191

Table C.4. uC/OS System Service in ACSR (cont'd) 192

Table C.5. DCM∥uCOS System Service in ACSR 193

Table C.6. DCM∥uCOS System Service in ACSR (cont'd) 194

Table C.7. DCM∥uCOS System Service in ACSR (cont'd) 195

Table C.8. DCM∥uCOS System Service in ACSR (cont'd) 196

Table C.9. DCM∥uCOS System Service in ACSR (cont'd) 197

Table C.10. DCM∥uCOS System Service in ACSR (cont'd) 198

Table C.11. DCM∥uCOS System Service in ACSR (cont'd) 199

Table C.12. DCM∥uCOS System Service in ACSR (cont'd) 200

Table C.13. DCM∥uCOS System Service in ACSR (cont'd) 201

Table C.14. DCM∥uCOS System Service in ACSR (cont'd) 202

Table C.15. DCM∥uCOS System Service in ACSR (cont'd) 203

Table C.16. DCM∥uCOS System Service in ACSR (cont'd) 204

Table C.17. DCM∥uCOS System Service in ACSR (cont'd) 205

Table C.18. DCM∥uCOS System Service in ACSR (cont'd) 206

Figure 1.1. Our Approach 19

Figure 3.1. EarIy Warning system in Statecharts 37

Figure 4.1. Embedded Software Modeling Framework using Statecharts and TRoS 50

Figure 4.2. A Gate Controller Model in Statecharts and TRoS 53

Figure 4.3. Timed Behavior Models in TRoS 55

Figure 4.4. An Example of TRoS 58

Figure 4.5. Timed Behavior of TRoS 61

Figure 4.6. Syntactic Sugar for Timed Actions 69

Figure 4.7. Railroad Crossing Gate Controller's Behavior Model 71

Figure 4.8. An Example of Producer and Consumer 72

Figure 5.1. Our Approach 76

Figure 5.2. Specifications of ACSR and Statecharts for OSSemPend 77

Figure 5.3. An Example of TRoS∥ACSR 78

Figure 5.4. Application Software Models in Statecharts and TRoS 85

Figure 5.5. Three Tasks in Communication 87

Figure 5.6. Three Tasks in TRoS∥ACSR 88

Figure 6.1. Our Platform-based Development using TRoS∥ACSR 94

Figure 6.2. APEX Interface in IMA 96

Figure 6.3. ARINC 653 Process Model 99

Figure 6.4. Control Flow in TRoS 100

Figure 6.5. Two Processes in TRoS and Semaphore Service in ACSR 104

Figure 6.6. A Flight Application : ON_FLIGHT 105

Figure 6.7. Basic Functional Requirement of Position Indicator in Statecharts 107

Figure 6.8. Statecharts Specification of POSITION_INDICATOR based on Platform-provided System Services 110

Figure 6.9. Un-timed TRoS Requirement Specification of POSITION_INDICATOR 111

Figure 6.10. TRoS Specification of POSITION_INDICATOR 119

Figure 6.11. Syntactic Sugar for Preemptive and Non-preemptive Timed Actions 122

Figure 6.12. Transformation of TRoS nodes into Graphical ACSR nodes 123

Figure 6.13. POSITION_INDICATOR in Graphical ACSR 124

Figure 6.14. Verification Result: Deadlock 127

Figure 6.15. Verification Result: Counter Example for Deadlock 127

Figure 6.16. Verification Result: Deadlock Trace 128

Figure 6.17. Erroneous Specification in ON_FLIGHT 129

Figure 6.18. Verification Result of Corrected ON_FLIGHT Specification 129

Figure 7.1. Our Approach to Behavior Models for MDA 136

Figure 7.2. An Example of Permissive Moving Authority (PMA) Setting 141

Figure 7.3. PIM Behavior Models of DCM 143

Figure 7.4. PIM and PSM for Verify Train Position 145

Figure 7.5. Errors in DCM Model Behaviors 146

Figure 7.6. The Result of DCM's Timing Verification 148

Figure A.1. Functional Requirement Models of ON_FLIGHT in Statecharts 154

Figure A.2. Requirement Specification Model of POSITION_INDICATOR in Statecharts 155

Figure A.3. Requirement Specification Model of FUEL_INDICATOR in Statecharts 156

Figure A.4. Requirement Specification Model of PARAMETER_REFRESHER in Statecharts 157

Figure A.5. Formal Untimed Requirement Behavior Model of ON_FLIGHT in TRoS 158

Figure A.6. Timed Requirement Behavior Model of POSITION_INDICATOR in TRoS 159

Figure A.7. Timed Requirement Behavior Model of FUEL_INDICATOR in TRoS 160

Figure A.8. Timed Requirement Behavior Model of PARAMETER_REFRESHER in TRoS 161

Figure A.9. POSITION_INDICATOR in ACSR 1 162

Figure A.10. FUEL_INDlCATOR in ACSR 1 163

Figure A.11. PARAMETER_REFRESHER in ACSR 1 164

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.