Model checking timed properties of healthcare processes

Keith Miller; Wendy MacCaull

doi:10.1002/smr.527

Model checking timed properties of healthcare processes

Journal of Software Maintenance and Evolution Research and Practice ◽

10.1002/smr.527 ◽

2011 ◽

Vol 23 (4) ◽

pp. 245-260 ◽

Cited By ~ 1

Author(s):

Keith Miller ◽

Wendy MacCaull

Keyword(s):

Model Checking ◽

Healthcare Processes ◽

Timed Properties

Download Full-text

Observer Patterns for Timed Properties

International Journal of Software Innovation ◽

10.4018/ijsi.2021040101 ◽

2021 ◽

Vol 9 (2) ◽

pp. 1-17

Author(s):

Djamila Baroudi ◽

Safia Nait-Bahloul

Keyword(s):

Model Checking ◽

Embedded System ◽

Formal Methods ◽

Reachability Analysis ◽

Domain Specific Language ◽

Formal Specifications ◽

Specific Language ◽

Domain Specific ◽

Formal Techniques ◽

Timed Properties

Dwyer et al. proposed qualitative specification patterns that enable the practitioners of model checking tools to write formal specifications mainly used for automatic model checking. Although this involves formalisms that are not always easy to handle by engineers, to facilitate the integration of formal methods based on these definition patterns in the industrial field, several formal techniques and languages have been proposed. This paper studies a domain specific language named CDL which help non-experts writing formal specifications effortlessly. In CDL, a property is transformed into an observer automaton to perform a reachability analysis. The existing CDL patterns allow non-experts to reason about occurrence and order of events, but not enough about their timing. Furthermore, the semantics of patterns and transformations are not ideally formalized and are still complex. This work serves to extend the existing CDL system by patterns related to time. The contribution is illustrated in an industrial embedded system.

Download Full-text

Characterizing Compatibility of Timed Choreography

International Journal of Web Services Research ◽

10.4018/jwsr.2011040101 ◽

2011 ◽

Vol 8 (2) ◽

pp. 1-28 ◽

Cited By ~ 6

Author(s):

Nawal Guermouche ◽

Claude Godart

Keyword(s):

Model Checking ◽

Web Services ◽

Application Integration ◽

Business Organizations ◽

Compatibility Analysis ◽

Collaborative Processes ◽

Service Oriented ◽

Multiple Services ◽

Quantitative Properties ◽

Timed Properties

Web services are the main pillar of the Service Oriented Computing (SOC) paradigm which enables application integration within and across business organizations. One of the most important features of Web services is the idea of choreography which captures collaborative processes involving multiple services. In this context, compatibility analysis of choreography is a central point to investigate. The compatibility of a choreography means the capability of a set of Web services to interact by exchanging messages in a safe way. Whether a set of services are compatible depends not only on their sequences of messages but also on quantitative properties like timed properties. In this paper, the authors investigate a model checking based approach that checks the compatibility of a choreography in which Web services support asynchronous timed communications.

Download Full-text