ASADAL/SIM: An incremental multi-level simulation and analysis tool for real-time software specifications

Abstract

Despite considerable advancement in software engineering methods during the past three decades, requirements engineering of large and complex software systems still remains a difficult and active research problem. One such difficulty lies in developing correct and useful methods for the validation and verification of real-time software specifications. One way of analyzing and validating/verifying software specifications is to mathematically derive or prove desired system properties based on formal specification languages. A full scale system analysis using such formal methods is limited in practice because of the required mathematical skills and computational costs. Formal methods are often used to check only a few very critical real-time properties. Simulation is a complementary approach to testing various system characteristics and validating user requirements. It is especially good for providing a rough picture of final system behavior. This paper presents ASADAL/SIM, a tool for multi-level simulation and analysis of real-time software specifications. It is a subsystem of a larger computer-aided real-time software development environment called ASADAL, and complements ASADAL/PROVER, another subsystem of ASADAL which is a formal verification module.(1) With ASADAL/SIM, simulation primitives can be added to evolving specifications in order to assign stochastic behaviors to external entities and internal processes, and to build a simulation model. ASADAL/SIM can execute the model and, at the same time, demonstrate the final system behavior by graphically showing internal workings of the system; catch undesirable system behaviors with breakpoints; and present various analytical results and system statistics. ASADAL/SIM, following ASADAL's philosophies of hierarchical system modeling and early system validation, allows users to simulate 'evolving' specifications at different, mixed, and wide levels of detail. In particular, algorithmic details may be specified for low level behavioral blocks, and simulated with abstract entities yet to be refined to such a level. This facilitates the tracking of critical data values at the specification level, and eases the next transformation into code level implementation. With ASADAL/SIM, ASADAL becomes an effective and comprehensive supporting tool for various existing software engineering approaches, particularly top-down refinement and incremental development practices. (C) 1998 John Whey & Sons, Ltd.