KENNESAW STATE UNIVERSITY

DEPARTMENT OF COMPUTER SCIENCE AND INFORMATION SYSTEMS

Yamacraw Research Project

"A Light-weight Approach with Formal Specification of Real-Time Systems"

Dr. Jose M. Garrido

 GENERAL

Papers and documents

A light-weight method and supporting environment for using formal and empirical techniques to analyze, apply simulation to verify real-time software systems from requirements specifications.

The overall in software engineering is the development of reliable and trustworthy real-time systems. This document proposes a general approach for specifying and then modeling real-time systems.

The three basic parts of the proposed research are:

• Proposal of a logic for OCL to be used in the formal specification of real-time systems
• Developing an extended version of OCL for real-time systems.
• An approach and technique to include simulation models in the verification of the specification.

Standard notations and concepts are to be used for this work. OCL has been proposed by OMG to complement UML. The simulation language to be used is Java, a standard programming language.

Current practice in industry has shown that on one extreme ad-hoc development techniques are still applied in development of real-time systems. On the other extreme, large corporations that apply formal methods have realized that these are extremely difficult to apply to large and complex systems.

This proposal is based on the hypothesis that a development method for large and complex systems (real-time systems) must include:

• Formal methods;
• Empirical methods (i.e., simulation);
• Object-oriented modeling techniques.

The outcome of this project will be:

• A method to specify real-time systems using a light-weight approach: through a notation that is a real-time extension to UML.
• A method and supporting software for the simulation of the specified real-time system, as the verification of the specification.

Specification Levels

1. Formal specification, with OCL

2. Operational specification, with RT-UML using an operational semantics.

Verification

1. Language acceptance in grammar of specification language. (Not yet considered.)

2. Automatic analysis of traces as a history of events from simulation runs.

Formal proofs, a mathematical certainty of the correctness of design with respect to a specification. It is a labor-intensive, costly, error-prone activity (requiring highly skilled people). Automatic verification can be performed only with reference to finite domains because the problem is unsolvable in the general case. In practice, only critical parts of a system can formally be verified.

With simulation, the traces of simulation runs are recorded and checked for consistency with respect to the specification by means of a history checker. The implementation of the system can be considered a refinement of the simulation model.

Without formal methods, real-time systems can be developed, but the total development time is long, and the process is expensive. Corporations using formal methods have produced designs with a higher quality and decreased cost because of shorter testing times.

In the near future, more emphasis will be placed on integrated formal development environments. More and better education and training is necessary for engineers. The practical purpose of applying formal methods is to reduce the risk of serious errors in specification and design. The cost of full verification is prohibitive, and early detection of errors is a more realistic goal. In more clear terms, finding bugs (early) is a much more achievable goal than trying to guarantee correctness. The conceptual gap between application domains and mathematics must be bridged by building mathematical models of the application domains.

This work will build, in part, upon KDL developed at California Institute of Technology and the work on simulation and DEVS carried out by Prof. Zeigler at the University of Arizona.