Title: | Specification and Analysis of Distributed Object-Based Stochastic Hybrid Systems |
Author(s): | Meseguer, José; Sharykin, Raman |
Subject(s): | distributed systems |
Abstract: | In practice, many stochastic hybrid systems are not autonomous: they are objects that communicate with other objects by exchanging messages through an asynchronous medium such as a network. Issues such as: how to compositionally specify distributed object-based stochastic hybrid systems (OBSHS), how to formally model them, and how to verify their properties seem therefore quite important. This paper addresses these issues by: (i) defining a mathematical model for such systems that can be naturally regarded as a generalized stochastic hybrid system (GSHS) in the sense of [7]; (ii) proposing a formal OBSHS specification language in which system transitions are specified in a modular way by probabilistic rewrite rules; and (iii) showing how these systems can be subjected to statistical model checking analysis to verify their probabilistic temporal logic properties. |
Issue Date: | 2005-10 |
Genre: | Technical Report |
Type: | Text |
URI: | http://hdl.handle.net/2142/11116 |
Other Identifier(s): | UIUCDCS-R-2005-2649 |
Rights Information: | You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s). |
Date Available in IDEALS: | 2009-04-20 |