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 ofactivities that have timing and resource constraints. A TRSBPseems simple, but its analysis needs to consider what are not explicitly mentioned as activities and may introducea 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, and describe how to specify and analyze formalized TR-SBPs (Formal TR-SBPs) using Alloy.