eXtended Reactive Modules

Authors

Benoît Sigoure

Type

techreport

Year

2006

Number

0620

Projects

APMC, Spot

Keywords

model-checking, XRM, eXtended Reactive Modules, PRISMAPMC, Stratego/XT, program transformation

Abstract

Reactive Modules is a formal model used to represent synchronous and asynchronous components of a system. PRISM is a widely used probabilistic model-checker. It introduced the PRISM language, highly based on the Reactive Modules formalism. This language quickly reaches its limit when it comes to large models. eXtended Reactive Modules (XRM) is an extension of the PRISM language. It comes with a compiler that translate XRM modules in PRISM modules, thus providing a comprehensive and reliable solution for people willing to write large models.