Real-Time System Specification and Verification
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 30, 1988
- Accession Number
- ADA214049
Entities
People
- K. T. Narayana
Organizations
- Pennsylvania State University