Verification of Timed Healthcare Workflows Using Component Timed-Arc Petri Nets

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BERTOLINI Cristiano LIU Zhiming SRBA Jiří

Year of publication 2013
Type Article in Proceedings
Conference Proceedings of the 2nd International Symposium on the Foundations of Health Information Engineering and Systems (FHIES'12)
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-39088-3_2
Field Informatics
Keywords verification; timed workflows; healthcase case study
Description We present a new automata-based interface model describing the interaction behavior of software components. Contrary to earlier component- or interface-based approaches, the interface model we propose specifies all the non-blockable interaction behaviors of a component with any environment. To this end, we develop an algorithm to compute the unblockable interaction behavior, called the interface model of a component, from its execution model. Based on this model, we introduce composition operators for the components and prove important compositionality results, showing the conditions under which composition of interface models preserves unblockable sequences of provided services.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info