Watchdog Transformations for Property-Oriented Model-Checking
| Autor: | Michael Goldsmith, Tim Whitworth, Irfan Zakiuddin, Nick Moffat, Bill Roscoe |
|---|---|
| Rok vydání: | 2003 |
| Předmět: | |
| Zdroj: | FME 2003: Formal Methods ISBN: 9783540408284 FME |
| DOI: | 10.1007/978-3-540-45236-2_33 |
| Popis: | We discuss how to transform a CSP refinement, \(S \sqsubseteq I\), to enable all its events to be hidden; this is useful because many of the state space compression functions provided by the model-checker FDR are effective only when events are hidden [1]. In an earlier paper [2] we described a suitable transformation for the case where the refinement is in the traces semantics of CSP. This paper extends the approach to the more difficult case of the stable-failures semantics. In both cases, a watchdog transformation is applied to the specification S, resulting in a watchdog processWDS, which is then composed in parallel with I, or with I in a simple context. The watchdog process monitors I and somehow indicates whether it can behave in a way that is incompatible with refinement of S. All events of the original assertion can be hidden in the transformed assertion. We also discuss the design of compression strategies that try to hide as many events as possible in the component processes of I and WDS, and compress the composition as it is being built up. We describe our implementation of the watchdog transformations and some simple compression strategies. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|