Process algebraic approach to the parametric analysis of real-time scheduling problems

This thesis develops a general framework for symbolic analysis of real-time systems based on process algebra and demonstrates the usefulness of such a process-algebraic framework by applying it to the scheduling problems of real-time systems.; We have extended the Algebra of Communicating Shared Resources (ACSR) to ACSR with Value-passing (ACSR-VP) in order to model the systems that pass values between processes and change the priorities of events and timed actions dynamically. In order to capture the semantics of ACSR-VP process terms, we propose a Symbolic Graph with Assignment (SGA). We further presents new algorithms for computing symbolic weak bisimulation for ACSR-VP processes. These algorithms are built on the basis of a new formulation of late weak bisimulation which we propose in this thesis.; With ACSR-VP, a real-time process algebra with parameters and value-passing capabilities, we propose a unifying method for analysis of scheduling problems in real-time systems which allows us to model the system with unknown parameters. We defined the restricted syntax form for ACSR-VP process terms, which is decidable and general enough to model real-time scheduling problems. The specification in the restricted form is analyzed by means of a symbolic algorithm. The outcome of the analysis is either (1) a set of predicate equations, (2) a boolean expression, or (3) a set of boolean equations and, if it exists, the solution to them identifies under what values of the unknown parameters the system becomes schedulable. To solve a set of predicate equations with unknown parameters, we demonstrate the use of constraint logic programming techniques. A boolean expression with unknown parameter can be solved by integer programming tools, and we present an algorithm to solve a set of boolean equations with unknown parameters.; With our new framework the scheduling problem in real-time systems is reduced to the problem of solving predicate equations, a boolean expression, or a set of boolean equations. A solution to them yields the values of the parameters that make the system schedulable. To facilitate the use of our approach in the design and analysis of scheduling problems, we developed a tool called PARS (Parametric Analyzer for Real-time Systems). Our framework is illustrated with substantial examples and case study.