Societal processes, such as those used in healthcare, typically depend on the e ective utilization of resources, both human and non-human. Sound policies for the management of these resources are crucial in assuring that these processes achieve their goals. But complex utilization policies may govern the use of such resources, increasing the di culty of accurately incorporating resource considerations into complex processes. This dissertation presents an approach to the speci cation, allocation, and analysis of the management of such resources.
Complex real-world processes with human, software, and hardware resources integrated to perform key functions, play an important role in our society. Because access to these resources is usually limited both by their quantity and by restrictions on their availability, contention for them is often a serious problem. Understanding how such contention arises requires that these process speci cations be su ciently powerful and precise to specify just how process activities make use of these resources. This is further complicated by the need to also precisely de ne potentially complex and numerous resource allocation policies that are driven by process goals, regulations, or the need to satisfy the interests of di erent stakeholders. For instance, hospital emergency department (ED) processes use diverse resources, such as medical sta , beds, and devices that are often severely limited in quantity and are restricted by policies that often conict. For example, in many EDs, a patient should be cared for by the same doctor and nurse for the entire stay, but under unusual circumstances this policy may be violated to improve e ciency in patient care. Suboptimal policies for resolving hospital resource management con icts can result in such problems as overcrowding, ine cient sta utilization, and long length of patient stay.
Process resource management has been widely studied through modeling
and analysis, but most prior work has used relatively simple resource models
that have di culty specifying the necessary complex resource concerns exibly
and rigorously. This dissertation provides a framework for the speci cation and
analysis of resources and their utilization policies in such complex processes.
The research makes the following main contributions: (
Our resource modeling approach relies on a precise, well-de ned process model. For the ED domain, this means a detailed model of the process by which patients are treated. We use the Little-JIL language [6] to specify this model. Little-JIL process de nitions use hierarchical decomposition, exception handling, concurrency and human choice to structure process activities, where each activity incorporates the speci cation of the resources needed to perform the activity.
Our resource speci cation is orthogonal to, and separate from, activity and data ow speci cations. A resource is modeled as the composition of a set of attributes and a set of capabilities. A resource's attributes, e.g., age, experience, model number, memory footprint, and skill level, are used in deciding which resource instance is assigned to a requesting activity. One particularly important attribute in an ED domain is the work shift, specifying the times when a resource can be allocated to an activity. A resource's capabilities are the activities that the resource can perform. For example, a set of capabilities of a doctor (MD) includes prescribing medications and ordering tests.
Given the existence of such resource speci cations, this approach enables speci cation of three di erent kinds of resource utilization policies: permission constraint policies, scheduling policies, and con ict resolution policies. A permission constraint policy speci es the permissibility of a resource to handle a request as restricted by a speci ed guard (de ned as a Boolean expression). For example, the SameMD policy can constrain the choice of MD who can handle a request a speci c patient, and the ShiftMD policy can constrain the times when an MD can treat a patient. Schedule policies support the speci cation of contention and selection policies. Contention policies specify precedence among requests.
In a hospital ED, when multiple patient care activities for di erent patients require the service of more MDs than are currently available for allocation, an appropriate scheduling policy is necessary to resolve the contention problem among the requests. The selection policy complements the contention policy, supporting speci cation of precedence among the resources that are able to handle a resource request. For instance, when a new patient arrives in an ED, there are usually more than two MDs who can assess the patient. An appropriate workload policy can balance the workloads of the MDs. Con ict resolution policies specify how to deal with policies that come into con ict with each other and with the situation where two or more policies cannot be enforced simultaneously. For instance, patient hando in a hospital ED is speci ed by using a con ict resolution policy because MDs are not able to satisfy both the SameMD and ShiftMD policies at the ends of their shifts [2, 4]. 3
The process- and resource-aware DES framework supports the execution of
simulations of processes whose activities are modeled in Little-JIL, and whose
resources are modeled in the resource modeling approach presented in this
dissertation by extending JSim [3]. The extension enables the simulator to support
scenarios such as (
The dissertation presents a novel constraint-aware resource scheduling approach that consists of three steps. First, an algorithmic control method embedded within the resource-aware DES framework computes resource requirements, such as how many of each resource must be present at each time epoch to meet user-speci ed resource utilization requirements. Second, deterministic Integer Linear Programing (ILP) produces a resource schedule that satis es those resource requirements and user-speci ed constraints on resource utilization. Finally, the resource-aware DES computes how the resource schedule a ects statistical estimates of the system's runtime properties. 4
This process- and resource-aware DES framework shows promise as a vehicle for evaluating diverse resource utilization policies in a exible manner. However, the dynamic approach veri es only that a single simulation adheres to the resource utilization constraints, but it is inherently unable to assure that all possible simulations adhere to the constraints. The dissertation develops a novel approach to analyzing the application of resource utilization policies statically.
Model checking is a static analysis technology that has long been used to either demonstrate that all possible executions of a program adhere to speci ed properties, or to identify counterexample executions that violate a property, e.g., FLAVERS [1]. Typically, the properties are event sequence speci cations characterizing program functionality. This dissertation uses this technology to statically verify that all simulation executions adhere to resource utilization properties, increasing the credibility of the simulation studies and their applicability in practice.
As with other model checking tools, FLAVERS requires three kinds of inputs: a detailed and rigorously-de ned ow graph, a property nite state machine (FSM), and a set of constraint FSMs. Given the precise speci cations of resources and their utilization policies, the process- and resource-aware model checking approach presented in the dissertation augments the three activityfocused inputs to FLAVERS with resource utilization speci cations, rigorously de ning feasible and infeasible resource allocations and utilization policies. This enables FLAVERS to verify that resource utilization policies must always be adhered to by all possible simulation runs. As an example, the dissertation presents a veri cation that a speci ed ED patient care process satis es the SameMD and shift policies. This static analysis approach has also been used to support reachability analyses that have detected the presence in some example processes of resource-driven deadlocks and con icts among policies. 5
The dissertation presents an evalu- RN Utilization (BMC) RN Utilization (New) ation of the resource modeling and 1980000 analysis approach by applying it to )(%7600 the challenging study of a detailed iilitzano 5400 hospital ED process. The ED pro- tU2300 10 cess model is based on real-world data 0 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 and the knowledge of a domain ex- Time (hours) pert with extensive experience as an Fig. 1. Utilization comparison over 24 emergency department physician and hours a day: RN Utilization (BMC) RN ED manager at the Baystate Medical utilization of Baystate Medical Center, RN Center (BMC), in Spring eld, MA, Utilization (New) RN utilization derived by USA. MD and nurse (RN) resources the constraint-aware scheduling approach are scheduled simultaneously while adhering to the complex characteristics of the ED such as time-varying patient arrivals, constraints and policies of medical providers, other hospital resource (e.g., beds) utilization, and complex patient care processes. The evaluation demonstrates that this scheduling approach creates better sta ng than existing real-world sta ng in terms of balancing resource utilization over a 24-hour period (see Fig. 1).
The DES framework provides detailed trace information about resource utilization to support the dynamic analysis of di erent resource utilization policies. However, this dynamic analysis is valid only when all the simulations of resource utilization adhere to the de ned resource utilization policies. Therefore, the dissertation also includes a demonstration that the formality of the resource speci cation supports veri cation of resource properties such as the absence of violations of resource utilization policies and the absence of deadlock. Given the entire ED speci cations, the static analysis approach veri es the adherence to the SameMD and ShiftMD policies; and nds con ict among hospital policies or detects a resource deadlock under various speci cation of the numbers of MDs, RNs, beds, and patients. Complex societal processes integrate multiple types of resources, such as humans, software, and hardware, to support the performance of process activities. Participation by these resources is often restricted by diverse resource utilization policies. Further, policies may at times con ict with each other, requiring conict resolution strategies that add extra complexity. Resource utilization policies usually signi cantly impact system behaviors and results. Therefore, resource utilization policies should be thoroughly evaluated and rigorously analyzed.
This dissertation presents a novel approach to create speci cations of policies that are su ciently precise and detailed to support static and dynamic analyses of how these policies a ect the properties of processes that are governed by these policies. The presented process- and resource-aware DES framework supports simulations of such processes that adhere to resource speci cations. The framework's evaluation of hospital ED processes demonstrated that it supports considerable exibility in resource and utilization policy speci cation and provides powerful dynamic analyses. However, the approach is inherently limited because of the impossibility of exhaustive simulations of all scenarios. To complement the dynamic simulation approach, this work develops a process- and resource-aware static analysis approach that globally veri es system properties and adherence to resource utilization policies. In doing this, the dissertation demonstrates how the speci cation and analysis framework can be e ective in guiding domain experts towards sound decisions about policies for the management of hospital resources, while also providing rigorously-based assurances that the guidance is reliable and well-founded.