Real-Time System Specification and Verification
PENNSYLVANIA STATE UNIV UNIVERSITY PARK WHITMORE CHEMICAL LAB
Pagination or Media Count:
We have developed a formal semantic model for real-time concurrency under limited parallelism. The model addresses memory access mechanisms, limited parallelism under asynchronous processors. In the framework of the model, various scheduling paradigms can be imposed. We formulated a language concept of tri-sections. The concept combines nondeterministic multiway synchronization of processes and processor holding into a single primitive construct. The use of the concept has been demonstrated with a process control system, resource allocation problems, and elevator systems. The concept allows the construction of maximally parallel regions in an otherwise limited parallel execution model. In a semantic sense, the achieves a reduction in the complexity of the limited parallelism models. We provided a formal design of a dialog system using the Z notation. Dialog systems are very much like operating system in the concepts they provide. The specification addresses the invariant properties which need to be satisfied by the various components of the system. In particular, the properties address object relationships in regard to their layout on the graphical interface, presentation of the visual aspects of the objects, activation and execution of programs attached to the objects, and concurrency supported by the system.
- Computer Programming and Software