Stochastic Charon

 

·       Overview

Stochastic Charon is a language for modular specification of interacting stochastic hybrid systems based on the notions of agents and modes. The language supports the operations of agent composition for concurrency, hiding of variables for information encapsulation, and instantiation of agents for reuse.

 

·       People

o       Mikhail Bernadskiy

Email: mbernads@gradient.cis.upenn.edu

o       Raman Sharykin

Email: rsharyki@math.upenn.edu

Homepage: http://www.math.upenn.edu/~rsharyki

o     Prof. Rajeev Alur

Email: alur@cis.upenn.edu
Homepage: http://www.cis.upenn.edu/~alur

 

 

·       Examples

o      Air Traffic Control

We model a system of two aircrafts flying from two airports and estimate the probability that these aircrafts will come to a particular minimum distance between them during their flights.

Charon code

 

o      Hard Drive Modeling

We model a hard drive for three values of a parameter of the power management policy and estimate the probability that a service request will be lost.

Charon code