Applying Empirical and Formal Methods for Modelling Systems with Concurrency and Timing Aspects

Software systems with concurrency are very complicated because they consist of many components that run in parallel and there can be a large number of combinations of how the components can interact. Deadlock, livelock, and other behavior can easily get out of control. Timing aspect adds another degree to the complexity. A pragmatic approach is presented for improving the specification and modelling of concurrency and timing by combining the use of the formal specification language Timed Communicating Object Z (TCOZ) and object-oriented simulation with OOSimL. The specification language TCOZ is well-suited for specifying complex systems that include components with their own thread of control. Object-Oriented simulation with OOSimL provides a powerful approach and tool for modeling large and complex systems and is compatible with the CSP semantics of concurrency. The output of the simulation runs provide traces of the timed interactions that can be used for verification with respect to the specification of the system. There is a simple and consisting correspondence from a formal specification to the corresponding simulation modelling. A simple problem is specified with TCOZ and the simulation model implemented with OOSimL is used to carry out simulation runs. This problem consists of three concurrent processes communicating among themselves and with the environment, subject to timing constraints.