Modeling and Formal Analysis of Real–Time System via CCS

Availability and reliability are of utmost important elements for real time systems. Availability means feasibility and compatibility of a system while reliability maintains a robust performing of a system. Most researches that related to real-time analysis have focused on the correctness but ignored the issue of compatibility, especially for substitutability of the involving tasks. Compatibility of tasks in real time system indicates the fitness of tasks that interact with each other, and substitutability is closely related to the fault tolerance mechanism of a system. In practice, one always applies backup tasks or ignored subtle fault of a task, to maintain a robust and continuation performing of a system. However, the replacement of a task or the ignored fault should not effect the main function. Thus, this would be important for us to analyze the substitutability. In this paper, we designed an Interrupt Driven Task Scheduler, which is formally modeled by a process algebra called CCS in 4 components, and analysis its correctness with the help of model checking. For more important, we described single tasks in CCS and analysis its compatibility in weak and strong levels and proposed algorithm for task compatibility checking. We then used the definition of compatibility to analysis substitutability of tasks with the help of observational equivalence of CCS.