An approach to modeling and verification of real-time systems

In the article an approach to modeling and verification of real-time systems is presented. Specification PEARL description language in used for IIW / SW modeling. It has its origins in the standard Multiprocessor PEARL language. Its usefulness has been enhanced for asymmetrical multiprocessor system modeling and parameters for schedulability analysis have been added. It is meant to be an over-layer for PEARL programs and supports the corresponding program model. The detailed program models are represented internally by Timed State Transition Automata. The model of the co-designed system is verified for feasibility with co-simulation. The resulting information may be used for changes in the current design to gain a feasible model of the system. After that the program models may be enhanced to their full functionality. Schedulability analysis, which should provide the designer with more precise timing information, shall then be done. The new timing information can be reused on the system model in order to disco ver bottlenecks or possible discrepancies with the estimated times. By utilising this methodology the possibility of implementing an infeasible system should be minimised.