Semantic Theories and Automated Tools for Real-Time and Probabilistic Concurrent Systems
Abstract
The main objective of this project was to develop new semantic theories and automated tools for real-time and probabilistic concurrent systems; that is, systems of coordinating processes that exhibit behavior of a probabilistic or statistical nature and which must meet real-time constraints. The main results achieved include a new semantic framework for reasoning about the relative reliability of probabilistic systems in different operating environments; an efficient algorithm for checking whether a specification of a real-time concurrent system satisfies a correctness property specified in a real-time temporal logic; and a new model of soft real-time systems that allows users to make rigorous statements about the likelihood with which systems are guaranteed to meet deadlines. A number of these results have been incorporated into the Concurrency Factory verification toolkit. In turn, the Factory has provided a platform for technology transfer with several Long Island companies, including Parker-Hannifin, Reuters America, and Northrop Grumman.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 23, 1997
- Accession Number
- ADA329736
Entities
People
- Scott A. Smolka
Organizations
- Stony Brook University