Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
A compositional modelling and verification framework for stochastic hybrid systems
Wang S., Zhan N., Zhang L. Formal Aspects of Computing29 (4):751-775,2017.Type:Article
Date Reviewed: Mar 29 2018

The need to explore new formalisms for specifying, implementing, and verifying systems is driven by the increasing complexity of systems we wish to analyze and synthesize. At the same time, there is a growing realization of the need for techniques to work in the context of incomplete knowledge. Probabilistic formalisms allow modeling incomplete knowledge of a system in the form of probability distributions and even enable some useful analysis of these systems.

This paper advances the state of the art by proposing a formalism--stochastic hybrid communicating sequential processes (SHCSP)--that can combine aspects of distributed systems, real-time physical systems, and probabilistic systems. It proposes a mechanism for combining mathematical formalisms for individual aspects into a coherent whole and delineates interactions between different aspects of the formalism. SHCSP is provided with an operational semantics that can be used for simulation. The authors also formulate sound axiomatic semantics for reasoning about properties of SHCSP processes. This is done from the ground up by first describing a logical language of assertions for describing properties and formulating sound rules of inference in the form of pre-/post-condition triples that can be used to reason about the evolution of SHCSP processes. The inference system is inspired by Hoare logic and assume-guarantee reasoning.

The material in the paper is quite dense and requires commitment in following up with the bibliography to understand the mathematical foundations of each aspect addressed in the paper: CSP, hybrid systems, and stochastic systems. The example provided in the paper is sketchy, and it is difficult to see how the rules of inference could be automated or could apply to larger examples--in particular, the compositional nature of the inference system is difficult to appreciate from the example.

Reviewer:  Prahladavaradan Sampath Review #: CR145939 (1806-0323)
Bookmark and Share
 
Specifying And Verifying And Reasoning About Programs (F.3.1 )
 
 
Stochastic Analysis (D.4.8 ... )
 
 
Model Development (I.6.5 )
 
 
Models Of Computation (F.1.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Specifying And Verifying And Reasoning About Programs": Date
Programming: the derivation of algorithms
Kaldewaij A., Prentice-Hall, Inc., Upper Saddle River, NJ, 1990. Type: Book (9780132041089)
Aug 1 1991
An introduction to programming with specifications
Kubiak R., Rudziński R., Sokolowski S., Academic Press Prof., Inc., San Diego, CA, 1991. Type: Book (9780124276208)
Jun 1 1992
Observational implementation of algebraic specifications
Hennicker R. Acta Informatica 28(3): 187-230, 1991. Type: Article
Jul 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy