If there is a suspicion of Lyme disease, a blood sample of a patient is sent to a medical laboratory. The laboratory performs a number of dierent blood examinations testing for antibodies against the Lyme disease bacteria. The total number of dierent examinations depends on the intermediate results of the blood count. The costs of each examination is paid by the health insurance company of the patient. To control and restrict the number of performed examinations the health insurance companies provide a charges regulation document. If a health insurance company disagrees with the charges of a laboratory it is the job of the public prosecution service to validate the charges according to the regulation document. In this paper we present a case study showing a systematic approach to reveal faulty processes of a medical laboratory. First, files produced by the information system of the respective laboratory are analysed and consolidated in a database. An excerpt from this database is translated into an event log describing a sequential language of events performed by the information system. With the help of the regulation document this language can be split in two sets - the set of valid and the set of faulty words. In a next step, we build a coloured Petri net model corresponding to the set of valid words in a sense that only the valid words are executable in the Petri net model. In a last step we translated the coloured Petri net into a PL/SQL-program. This program can automatically reveal all faulty processes stored in the database.
application of the regulations have to be proven to the health insurance companies. If a suspicion about irregular application of the regulations arises, it is the job of the public prosecution service to validate the billed charges according to the regulation document. Usually, the prosecution service orders a report investigating the issue from an expert-oce.
In this case study we describe an approach using coloured Petri nets which is inspired by the methods of the area of process mining and process discovery to reveal faulty processes given in log-files of a medical laboratory. The files contain data recorded over a period of five years having 1500-2000 orders a day. Each order consisting of 20-30 events, examinations and results. Altogether, we face about 100 million lines of log that need to be analysed and verified. Each line describes an event or a sub-process of the medical laboratory. Each event refers to the occurrence of an action of the information systems and is annotated with a time stamp, order-id, variables etc. Typical actions of the system are register order, register requirements, register examination results, validate results, make invoice, archive order . . . . In addition to these basic actions, a medical laboratory is able to perform a huge number of dierent examinations. In this case study the prosecution service ordered a report revealing all faulty processes concerned with Lyme disease.
To reveal all faulty processes of a set of log-files we choose a four step approach. We call the first step consolidation step. The main goal is to develop a schema to integrate all the recorded files into a relational database. Using the same schema it is also easy to implement a view on top of the database tables. The view abstracts from redundant or superfluous information and reduces the data to events and results corresponding to processes considering Lyme disease. With the help of this view we are able to produce an event log, i.e. a sequence of events bearing only information about order-number, time-stamp and result.
The next step is called the formalization step. Each sequence of events corresponds to a sequence of actions. Each sequence of actions is called a word. The set of words is called the language of the event log. The main task in the formalization step is to split this language into two sublanguages, the set of valid and the set of faulty words. This has to be done manually with the help of the charges regulation document. Of course, this is a time consuming task, but we believe that it is very easy and hardly error-prone to classify single words. We could also try to directly build a model of regulations from the charges regulation document to classify the set of words automatically, but often the regulation document is given as plain text. Starting from such a description is error-prone and easily yield a model that does not fit the recorded event log regarding names of actions, values and level of abstraction. Remark, we only need to partition the set of words, we do not classify the complete event log. In the formalization step a set of valid sequences of actions is produced. We call this set the language of regulations.
The third step is called integration step. The language of regulations is
integrated into a coloured Petri net model. Such an integration can be supported
by synthesis or workflow mining algorithms. In our case study the language of
regulations is already highly compressed and settled, such that we construct a
corresponding coloured Petri net model by hand using the editor CPN-Tools
[
The fourth step is called implementation step. Coloured Petri nets are well readable and have an intuitive formal semantic. We will show how to translate such a coloured Petri net model into a PL/SQL-program. We translate transitions to functions, places to tables and arcs to delete or insert statements. With the help of such a PL/SQL-program all sequences of events can be replayed in the database. If the replay fails, the sequence corresponds to the occurrence of a faulty process of the medical laboratory.
Figure 1 depicts an overview of the presented approach. A key feature is that it is built on a chain of formal models. The initial models, i.e. the schema, the view and the event log, consolidate the recorded data. Afterwards, the language of regulations, the coloured Petri net and the PL/SQL-program are build. The constructed models document of the whole inspection procedure, all results can easily be reconstructed, the produced models can be reused when inspecting other laboratories. Of course, stepping from one formal model to another highly supports the validity of the investigation report produced. Each step can be supported by algorithms and tools. Some steps can even run fully automated using e.g. synthesis algorithms for the construction of the Petri net model or automated generation of the PL/SQL-program.
The chosen approach is inspired by techniques well known in the area of
process mining where some recorded behaviour is merged into a formal model of
the underlying process [
The paper is organized as follows: Section 2 provides formal definitions. Section 3 presents the approach and our case study. In Section 4, we sum up the results to prove the applicability of the developed approach. 2
In this section we briefly recall the basic notions of languages, event logs and coloured Petri net.
An alphabet is a finite set A. The set of words over an alphabet A is denoted by Aú . The empty word is denoted by ⁄ . A subset L ™ Aú is called language over A.
Business processes describe the flow of work within an organisation [
Definition 1. Given a finite set of activities T , a finite set of values V and a finite set of cases C. An element ‡ oe (T ◊ V ◊ C)ú is called an event log. Fix a case c oe C we define the function pc : (T ◊ V ◊ C) ae (T ◊ V ) by pc(t, v, cÕ) = ; (t, v) ,if c = cÕ
⁄ ,else.
Given an event log ‡ = e1 . . . en oe (T ◊ V ◊ C)ú we define the language L(‡ ) of ‡ by L(‡ ) = {pc(e1)...pc(ei)|i Æ n, c oe C} ™ (T ◊ V )ú .
The language of an event log is finite and prefix closed. It reflects the control flow between activities given by the events of the log. Each case adds a word to the set of words called language.
In this paper we use coloured Petri nets to model valid behaviour of a
medical laboratory. The underlying Petri net models the control flow between
actions while variables control the examination results. The following definition of
coloured Petri nets was given in [
Definition 2. A coloured Petri net is a tuple CP N = (P, T, F, À, V, D, G, E, I ), where: P is a finite set of places.
T is a finite set of transitions, such that P fl T = ÿ holds.
F ™ (P ◊ T ) fi (T ◊ P ) is a set of directed arcs. À is a finite set of non-empty colour sets.
V is a finite set of typed variables such that T ype[v] oe À for all variables v oe V . D : P ae À assigns a colour set to each place.
G : T ae EXP V assigns a guard to each transition t such that T ype[G(t)] =
Bool.
E : F ae EXP V assigns an arc expression to each arc f such that T ype[E(f )] =
D(p)MS, where p is the place connected to the arc f .
I : P ae EXP 0 is an initialisation expression to each place p such that T ype[I(p)] = D(p)MS.
In contrast to low-level Petri net a place of a coloured Petri net belongs to a
given type called colour. According to this colour each place carries values called
tokens. Arcs carry variables and if an arc is connected to a place, the tokens
of the place can bind to variables of the arc. A binding b of a transition maps
variables of related arcs into values of related places. A transition t is executable
if there is a binding b such that the transition guard evaluates to true. When the
transition occurs, as for low-level Petri net, it removes the specified tokens from
the input places and produces tokens in the output places (see [
The initialisation function I assigns tokens to places yielding an initial marking. Given a coloured Petri net CP N a sequence of sequential enabled transitions is called an occurrence sequence of CP N . In this paper we add the values of the respective bindings to each transition of an occurrence sequence. The language L(CP N ) of CP N is defined as the set of all occurrence sequences. Given an event log log oe (T ◊ V ◊ C)ú , log is executable in CP N if L(log) ™ L(CP N ) holds. 3
In this section we present an approach to validate a set of given recorded files with the help of a regulation document. In the following case study, on behalf of the public prosecution service, recorded data of an information system of a medical laboratory has to be reviewed. During a period of five years 1800 files were produced and recorded. Each file contains about 1500 processed orders. The regulation document is given by a charges regulation document provided by health insurance companies. The goal is to identify faulty processes performed by the medical laboratory considering all processes corresponding to Lyme disease diagnostic. An overview of our approach is sketched in Figure 1 given in the introduction. The subsections of this section reflect the four steps of our approach. 3.1
In a first step the recorded files need to be consolidated and formalized. The aim of this step is to load the recorded files into a database to extract an event log from it afterwards. For the storage and processing of data, the commercial Oracle Database is used. This database system provides a procedural programming language named PL/SQL for the implementation of the stored procedures. To set up the database an entity-relationship diagram is produced. Of course, to produce this diagram first the recorded files need to be reviewed. Afterwards, we use the Oracle SQL Developer Data Modeler to construct the model.
An excerpt of a file recorded by the medical laboratory is depicted in Figure 2. All files of the laboratory’s information system have a hierarchical structure with a flexible record length up to 1024 characters. Each file is a sequence of dierent types of blocks. Each block corresponds to a set of dierent actions of the system. The first line of each block is the header of the block and all following lines are indented.
The file depicted in Figure 2 starts with a block corresponding to the registration of a new order for a blood count. The header of this block reads as follows: The first number corresponds to the registration-id 727980834 generated for this new order. This id perfectly fits the need to identify cases in the given file. In our case study each registration-id corresponds to a case of the system. The next two numbers refer to the time the registration occurred, i.e. January 25th 2011, 11:49:54 in our example. The next two strings indicate that this action was manually triggered. The last number of the header encodes the name of the action occurred. In this particular information system the number 10 refers to the action order blood count. The inner lines of this first block carry the values of this registration action. Possible values are the name, birthday and address of the patient registered.
The next block corresponds to the scheduling of examinations. The header refers to the same case as the first registration block since both ids match. Remark, both recorded actions even occurred within the same second. The difference between both headers is only given by the number at the end of the line. In this block 20 refers to the action schedule examination. This block consists of two sub-blocks, both sub-blocks marked by the keyword BORR. BORR stands for Lyme disease and indicates that the scheduled examinations are part of Lyme disease diagnosis. Again, the inner lines carry values of the scheduling where BORG and BORM are abbreviations of two dierent blood examinations. In this example the block corresponds to the occurrence of two dierent actions. A BORG-examination and a BORM-examination is scheduled.
The sixth block shown in Figure 2 corresponds to the recording of results of the scheduled examinations. The number 21 refers to the action receive result. This block matches the schedule examination block besides two important dierences. First, the keyword ONLVAL indicates that this event was automatically triggered by the information system when the results of examinations are received. Second, the inner lines of the block carry the results of these examinations. In this example the results of the BORG- and the BORM-examinations are received. The value of the BORG-examination is smaller than 10.00 and the value of the BORM-examination is smaller than 18.00. Both values show the absence of the corresponding antibodies, i.e. both examinations are negative and no further examinations need to be scheduled.
After knowing the structure of the files an entity-relationship diagram is built. With the help of this schema a PL/SQL-program is written to load all files into the Oracle Database. If all the data is stored, the next step is to extract a consolidated and formal event log from this database. The event log only contains events and values corresponding to processes that need to fulfil regulations given in the charges regulation document concerning Lyme disease diagnostic. We omit a detailed description of the produced entity-relationship diagram, but give a short impression in Figure 3.
Given the entity-relationship diagram it is easy to implement a view on top of the tables of the database to receive an appropriate event log. In our example, the excerpt depicted in Figure 2 only contains four blocks corresponding to Lyme disease diagnostic. In the first and in the third block two new orders arrived and both patients are registered. In the second block a BORG- and a BORMexamination for the first order is scheduled. The sixth block shows the results of both examinations. We are able to discard all other blocks shown in Figure 2. If we apply the constructed view to this excerpt we get the event log shown in Table 1. This event log abstracts from additional events and values. It shows the six events corresponding to the four blocks concerned with Lyme disease of Figure 2.
id
With the help of the Oracle Database and the implemented view arbitrary extracts of the recorded files can be shown as event logs. These logs are the results of the consolidation step of our approach. In the next steps these logs are filtered with the help of the regulation document and integrated to an executable model. 3.2
In the second step of our approach first the event log is used to define the formal language of the recorded behaviour. Then, in a next step, this behaviour is filtered with the help of the charges regulation document yielding a language of valid words. The aim of this formalisation step is to bring together the recorded behaviour and the regulation document given as plain text. Remark, that it is much easier to only evaluate the recorded language with the help of the regulations and not to build an independent model of all regulations hoping it will fit the language of the recorded behaviour.
To deduct a formal language from the event log, first the actions of the system need to be identified. In our case study the list of significant actions reads as follows:
T = {10, 20BORG, 20BORM, 20BV LSEG, 20BP 39G, 20BP 83, 20BIV 1, 20BIV 2, 20BIV 3, 20BIV 4, 20BOSP C, 20BV LSEM, 20BP 39M, 21BORG, 21BORM, 21BV LSEG, 21BP 39G, 21BP 83, 21BIV 1, 21BIV 2, 21BIV 3, 21BIV 4, 21BOSP C, 21BV LSEM, 21BP 39M }
The numbers 10, 20 and 21 indicate if a blood count for a patient is registered, an examination is scheduled or if a result is received. The attached letters are the abbreviations of the corresponding examinations. There are 12 dierent tests corresponding to Lyme disease diagnostic leading to 25 dierent actions in total. Every action having a name starting with 21 carries a value of the type boolean (i.e. either the examination is negative or positive). At this point we are able to abstract from any other value given in the files such that any other action occurs without additional data. As stated above all events having the same registrationid belong to the same case. Events of the same case can be ordered by their time stamp. If we apply this knowledge to our event log we get a set of words. The following table shows three example words given by the event log of our case study:
L(log) = {10 20BORG 20BORM (21BORG,false) (21BORM,false), 10 20BORG 20BORM 20BVLSEG 20BP39G 20BP83 20BIV1 20BIV2 20BIV3 20BIV4 20BOSPC 20BVLSEM 20BP39M (21BORG,true) (21BORM,true) (21BVLSEG,false) (21BP39G,false) (21BP83,false) (21BIV1,false) (21BIV2,false) (21BIV3,false) (21BIV4,false) (21BOSPC,false) (21BVLSEM,false) (21BP39M,false), 10 20BORG 20BORM 20BVLSEG 20BP39G 20BP83 20BIV1 20BIV2 20BIV3 20BIV4 20BOSPC 20BVLSEM 20BP39M (21BORG,false) (21BORM,false) (21BVLSEG,false) (21BP39G,false) (21BP83,false) (21BIV1,false) (21BIV2,false) (21BIV3,false) (21BIV4,false) (21BOSPC,false) (21BVLSEM,false) (21BP39M,false),
The language depicted in Table 2 was automatically processed from the given event log. This language is a complete and formal description of the set of processes occurred in the information system of the medical laboratory. Any new sequence of actions and values given by the events of a case yields a new word in the language of the log. Of course, the language of the log is much smaller than the event log since cases corresponding to the same process are not distinguished.
Given the language of the log the next step is to distinguish valid and faulty
words. This is a major task in the presented approach which can not be
automated. The charges regulation document is given as text. It is absolutely
necessary to understand the given regulations and apply them to the set of words. The
main advantage of the presented approach is that the set of words is given in a
very compact and formal style. There is no room for interpretations or
ambiguities. The rules of the charges regulation document do not need to be modelled
explicitly, they just need to be applied to the given language. As stated in [
In our example given in Table 2 the first two words are valid. The third word is faulty since the set of examinations {BVLSEG, BP39G, BP83, BIV1, BIV2, BIV3, BIV4, BOSPC, BVLSEM, BP39M } may only be preformed if one of the BORG- and BORM-examination is positive. According to the regulation document the blood count needs to be performed in two steps. First, the BORGand BORM-examination results need to be evaluated, if one of these is positive, a more detailed set of examinations should be performed.
The result of the formalization step is the set of valid words. This set can be seen as the relevant part of the language of the charges regulation document given in the language of the information system. If this language is found, the most challenging task of the investigation process has been completed. In the next steps this set is integrated into an executable model. 3.3
The third step of our approach is called integration step. The aim is to build
an executable model having the language of the charges regulation document.
As suggested in [
The problem of integrating a set of words into a Petri net is a well known
problem. There exists a lot of work tackling the problem in the area of process
mining [
In our case study our initial low-level Petri net contains 25 transitions corresponding to the 25 actions of our process identified in the formalization step. The control flow is rather simple and we just add the corresponding places. First, a blood count have to be registered, then an arbitrary number of the 12 examinations concerning Lyme disease can be scheduled. The execution of these 12 examinations must follow the simple rule, that first the BORG- and BORMexamination need to be performed before the other examinations occur. Remark, the control flow of the initial low-level net is independent form the values given in the language. Rules and regulation concerning values are added in the next step. All actions that corresponds to an examination result carry a value. For this reason we introduced a boolean colourset called RES and allow each such transition to be executed while binding to true or f alse. At this point we are able to require that a BORG- or BORM-examination must be positive before any other examination can be executed. In a last step we folded transitions if possible. The resulting net is depicted in Figure 4.
In Figure 4 the transition named 10 is enabled in the initial marking. If transition 10 fires, a BORG- and a BORM-token is produced in the place search test and tokens corresponding to all other examinations are produced in the place western blot test. In such a marking only the upper transition 20 is enabled. If transition 20 fires a BORG- or a BORM- examination is scheduled. As soon as an examination is scheduled transition 21 is enabled. If transition 21 fires, it consumes a token from the place investigation and moves this token to the place results. While the token is moved a random boolean value is attached. The lower transition named 20 is enable if the western blot tests are scheduled and if there are at least two tokens in the places results. The arc inscription 1Õy + +1Õz denotes a pair of tokens. One token is assigned to the variable y and another token is assigned to the variable z. The guard [fb(z)] ensures that the token called z carries the value true. It follows that in the model shown in Figure 4 the western blot tests can only be preformed if the results of the BORGand BORM-examination are present and at least one of these examinations was evaluated with true.
The model shown in Figure 4 is only able to reproduce one single run of the information system. In some sense it is a model of valid words, not a model of the running information system. Our goal is to replay each case of the event log in this model, there is no need to construct a model which is able to handle multiple cases at once.
Besides the possibility to validate the produced model by simulation,
CPNTools provides some model checking algorithms (see [
Liveness Properties ———————— Dead Transition Instances: None Live Transition Instances: None Fairness Properties ———————— No infinite occurrence sequences.
The integration step yields a sound and integrated model of the valid language produced during the formalization step. Of course, if analysing this model uncovers faults or additional requirements, the language produced in the formalization step needs to be adopted according to the change made in the model. If model and language match and describe the valid behaviour of the underlying charges regulation document, in the last step of our approach, the model is translated into executable PL/SQL-code. The fourth and last step of our approach is called the implementation step. Although, the coloured Petri net model is executable we translate the produced Petri net into PL/SQL-code. PL/SQL is a proprietary programming language which is integrated in the Oracle Database. Since it can execute SQL statements directly it is more suitable than Java or C++ in our approach. The aim is to get an executable program directly running next to the recorded data. With the help of this program faulty processes preformed by the medical laboratory can automatically be revealed.
During the case study the coloured Petri net model depicted in Figure 4 is transformed into PL/SQL mainly using the following ideas: (i) Each place of the coloured Petri net yields a temporary table in the database.
The tables are able to store records representing tokens and their values. (ii) Each transition of the coloured Petri net yields a parametrized function in the database. A function returns true only if the corresponding transition is executable. To check if a transition is executable arcs of the Petri net are translated into SQL-statements. Roughly speaking, these statements check if there exist appropriate values in the tables corresponding to places in the preset of the transition. (iii) Each arc of the coloured Petri net yields an SQL-statement in the database.
Arcs leading from a place to a transition correspond to DELETE-statements consuming tokens from tables. Arcs leading from a transition to a place correspond to INSERT-statements producing tokens in tables. (iv) Each guard or function of the coloured Petri net yields a function in the database. The SML-functions given in the coloured Petri net can easily be translated.
CPN
A table of transformation patterns is given in Table 4. With the help of these transformation rules it is even possible to implement a fully automated transformation procedure.
To actually verify the event log with the help of the PL/SQL-program the set of cases of the event log is replayed. The registration-ids of the set of faulty cases is stored in an additional table. With the help of this procedure faulty processes can be revealed. The set of faulty processes is the basis of the report produced for the prosecution service. The specific results produced in our case study are presented in the next section. 4
In the context of the presented case study, a set of files of a medical laboratory has been verified. The files record all occurred actions of the information system of the laboratory over a period of five years. In that given period, 22432 orders of Lyme disease diagnostic have been performed by the laboratory. The PL/SQLprogram produced by our approach calculates the following results: recorded processes 22432 valid 3311 faulty 19121 runtime 11 minutes
As shown in Table 5 only 15% of the recorded behaviour is valid according to the charges regulation document. It turned out, that the considered laboratory in almost every case performed the complete set of 12 examinations in a first step. The regulations require that the BORG- and BORM-examination precede all other examinations. Only if one of the two examinations is positive, the set of all examinations can be charged.
To get a more detailed view on the recorded data, in a second step, we adjusted our coloured Petri net model. We removed the transition guard requiring a positive result from one of the BORG- or BORM-examination, assuming a more sloppy interpretation of the regulation document. If we repeat the validation procedure we get that 50% of all recorded processes are valid concerning this more liberal model. In other words, even if we allow that all 12 examinations can be performed at once, 50% of all processes contain additional faults like unnecessary actions or manual changing of examination values.
In the paper we presented an approach together with a case study to verify logs revealing faulty processes of a medical laboratory. The produced PL/SQLprogram can directly be applied to any medical laboratory using the same information system. The main advantage of the presented approach is that it is based on a chain of formal models. With the help of these models it is easy to keep track of the validity of the produced report. Most of the steps can be supported using algorithms or tools well known in the area of Petri nets. Furthermore, experts on the regulation document can support the formalisation step without any knowledge about modelling techniques. If a model is produced it also can be adopted and reused. This can help to generate dierent criteria regarding only parts of the regulation document. Of course, all calculated results can be reproduced at any time, if this is required by the public prosecution service.
From the experience we gained in the case study we feel that the approach forces us to tackle the given task in a very structured way. The approach provides good documented, traceable results. In the future, we will test the presented approach on a larger regulation document yielding a larger regulation model and try to automate each step of the approach further.