Formal modeling and analysis of time- and resource-sensitive simple business processes

A time- and resource-sensitive simple business process (TR-SBP) consists of a finite set of finite series of activities that have timing and resource constraints. A TR-SBP seems simple, but its analysis needs to consider what are not explicitly mentioned as activities and may introduce a non-negligible number of intermediate states. In this sense, the analysis has similarities with security protocol analysis that needs to consider intruders. We formalize TR-SBPs as a round-based model called Formal TR-SBPs in this paper. We describe how to specify Formal TR-SBPs in Maude, a specification language based on rewriting logic and Alloy, a specification language based on first-order relational logic, and how to analyze Formal TR-SBPs based on those specifications with Maude and Alloy. A nursing problem is used as an example of TR-SBPs in this paper.