Formal description and verification of the OSEK/VDX specification in CafeOBJ

1.Library used for formal description and verification in CafeOBJ

1.1 Basic

1.2 LK

1.3 Partial order

1.4 Maximal elements of a non-empty partially ordered set

2.Formal description of the osek/vdx specification in CafeOBJ

2.1 A framework for formal description of the OSEK/VDX specification

2.2 Architecture of the OSEK operating system

2.3 Task management

2.4 Interrupt processing

2.5 Event mechanism

2.6 Resource management

2.7 Alarms

2.8 Messages

2.9 Error handling, tracing and debugging

2.10 Description of system services

2.11 Specification of operating system services

2.11.1 Common data types

2.11.2 Task management

2.11.3 Interrupt handling

2.11.4 Resource management

2.11.5 Event control

2.11.6 Alarms

2.11.7 Operating system execution control

2.11.8 Hook routines

2.12 Conformance classes

3 Verification