Specification and Analysis of Distributed Object-Based Stochastic Hybrid Systems

Meseguer, José; Sharykin, Raman

Permalink

https://hdl.handle.net/2142/11116 Copy

Description

Title

Specification and Analysis of Distributed Object-Based Stochastic Hybrid Systems

Author(s)

• Meseguer, José
• Sharykin, Raman

Issue Date

2005-10

Keyword(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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11116

Copyright and License 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).

Owning Collections