Specification and analysis of distributed object-based stochastic hybrid systems

José Meseguer, Raman Sharykin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 [6]; (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.

Original languageEnglish (US)
Title of host publicationHybrid Systems
Subtitle of host publicationComputation and Control - 9th International Workshop, HSCC 2006, Proceedings
Pages460-475
Number of pages16
DOIs
StatePublished - 2006
Event9th International Workshop on Hybrid Systems: Computation and Control, HSCC 2006 - Santa Barbara, CA, United States
Duration: Mar 29 2006Mar 31 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3927 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Workshop on Hybrid Systems: Computation and Control, HSCC 2006
Country/TerritoryUnited States
CitySanta Barbara, CA
Period3/29/063/31/06

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Specification and analysis of distributed object-based stochastic hybrid systems'. Together they form a unique fingerprint.

Cite this