Grading dozens of Petri net models manually is a tedious and error-prone task. In this paper, we present Grade/CPN, a tool supporting the grading of Colored Petri nets modeled in CPN Tools. The tool is extensible, configurable, and can check static and dynamic properties. It automatically handles tedious tasks like checking that good modeling practise is adhered to, and supports tasks that are difficult to automatize, such as checking model legibility. We propose and support the Britney Temporal Logic which can be used to guide the simulator and to check temporal properties. We provide our experiences with using the tool in a course with 100 participants.
Colored Petri nets (CPNs) [
The support required for grading assignments is similar to what is needed for testing or model checking, as we need to check a model against some formal requirements. As we aim at supporting grading for all kinds of models, we here focus on the testing perspective, as a model may not be suitable for model checking due to having a large or even unbounded state space. Thus, parts of the work described here is also applicable to general testing of CPN models, but we present it here in the context in which it was developed. The significant difference to classical testing is that for grading a possibly large set of different models is to be checked against the same specification in a uniform way.
CPN Tools [
There are as many ways of using models as there are teachers, so it is important that the requirements for the model can be described easily. This means that the grading tool must be configurable , allowing individual teachers to customize what is checked and how adhering to or deviating from each requirement is awarded or punished. In addition, it must be easily possible to extend the tool with new requirements. Thus our tool must have a plug-in like architecture allowing new requirements to be added with minimal effort. At the same time, we do not desire a heavy-weight framework with a steep learning curve just to add a simple custom requirement. Of course, such a tool should come with a set of reasonable built-in plug-ins so it is useful for many scenarios without requiring any programming. 1`"Book"++1`"Bike"++1`"Laptop" Inventory
To illustrate our motivation Product for developing such a tool, as- Order sume we want students to model Order ian(gsimCpPliNfied)Tdoeollisv.eryTsheerviicdeeaus-is Shop SRhieptmurennt Shipment ROefjfeecrt CxZxO Customer tporomduocdtesl frtohmat acusshtoomp,erasndordtheer IDxP DSeelrivveicrey Accept CCxxZZxxOO shop uses a delivery service to Notification Delivery deliver ordered products to the Shop OrderID DeliveryService Packet Customer customers. To this end, we would Fig. 1: Base model of a delivery service. provide students with a base model as in Fig. 1. The CPN in Fig. 1 models the behavior of the customer and the shop and provides the interface between customer and delivery service (Reject, Offer, Accept, and Delivery) and the interface between shop and delivery service (Shipment, Return, and Notification ). A customer can choose a product from the catalog and place an order via place Order. The shop prepares the ordered product for shipment and sends the resulting packet to the delivery service via Shipment. The delivery service shall in all tasks try to deliver packets to the respective customers via place Offer. If a customer is not at home, a token is placed on place Reject; otherwise, a token is produced on place Accept and, finally, the delivery service hands over the packet to the customer via place Delivery. Place Return is used to send a packet back to the shop in case the packet could not be delivered. In addition, the delivery service informs the shop via place Notification that a packet has been successfully delivered. The pages Shop and Customer are given but the DeliveryService is empty and intended to be modeled by the student.
When students are given such a base model, they are asked to model the missing part(s) or to change or improve the given model. These changes must adhere to certain constraints. In our example, we would need to be able to check that the given environment has not been changed (as the environment constitutes a contract with the external world) and that the model satisfies the given requirements, which often means that behavioral properties need to be checked. Our focus on the first version of our tool has therefore been on making it easy to check these requirements.
We have also implemented checks that ensure good modeling practise, including respecting data hiding (i.e., student solutions are not allowed to connect to nodes of the environment other than the interface places) and proper termination (i.e., ensuring that tokens are not erroneously left behind), and simple static analysis (e.g., ensuring that communication channels are used in the correct direction, i.e., no messages are produced on an input channel).
As we cannot check all properties mechanically—for example, whether the model is readable and understandable—we have implemented functionality facilitating this. This includes generating a view of the model in which the studentdesigned parts are highlighted and the given parts from Fig. 1 are dimmed. This allows teachers to focus on the new parts without having to distinguish these parts manually.
We have earlier encountered problems with students copying solutions from one another. We would also like to detect this, so we have checks that at least make it harder to cheat. This includes providing each student with a unique copy of the base model from Fig. 1 with a cryptographic signature including the student ID embedded. This makes it impossible to two students to use the same base model as starting point (indicating that one got a copy from the other).
Finally, we want a report summarizing all findings; the report should be useful for both teachers, who should be able to grade the model based on the report only, without having to manually open the model in CPN Tools except in special cases, and for students, who should be pointed to flaws in the model, using error traces when applicable.
We have chosen to implement our tool as a vanilla Java application. The
language is chosen due to its popularity and platform-independence. We have
chosen not to rely on a framework for handling plug-ins, as these frameworks
often demand significant overhead due to providing features we do not need
(e.g., we do not need dynamic configuration of plug-ins). We have used the
library Access/CPN [
To sum up, we need a tool that 1. Works with CPN Tools models, 2. Provides easy configuration, 3. Is easily extensible, 4. Contains a reasonable base set of capabilities, including: (a) Detect changes to a given environment, (b) Check dynamic properties using simulation, and (c) Check good modeling practise, including data hiding, proper termination, and provide simple static analysis, 5. Supports the manual part of the grading process, 6. Detects attempts to defraud, and 7. Provides a report that pin-points problems, aids the teacher in grading, and allows students to understand problems.
We continue with the outline of the architecture of our tool and introduce some simple plug-ins checking basic properties in Sect. 2. In Sect. 3, we introduce a temporal logic which is powerful enough to describe most dynamic requirements while still being easy to use. In Sect. 4, we sum up our experiences using our tool in semi-automatically assessing assignments from close to 100 students. Finally, we discuss related work, conclude the paper, and provide directions for future work. 2
Itnurtehiosf sGecrtaiodne/,CwPe Nou. tWlineefirtshtegaivrcehtitheec- li-gun1P li-gun2P il-ug3nP … il-ngunP ftorhvoiemsraslotlhlvaeersicnhrteirtqoeucdituruecrmteioenann.tsdT1he,ex2np,,la3wi,neanphdroow7- ((C(CCPPPNFNFNi)Fl)iel)MeiMlsMesooodddeeelll GradRee/pCoPrNting PPPDRDDRFeRFFe/pe/H/pHopHTorTotTMrsMrtMtLLL vide the details of some of the built- Configuration i4n(ap),lu4g(-cin),s, afnodcus6i.ngReoqnuirreeqmueirnetm5entiss ConfiFgiuleration AcceJsasv/aCPN CSPimNuTlaotoolrs handled partly in this section and in the next section, where we also deal Fig. 2: Overall architecture and enviwith requirement 4(b) (checking dy- ronment of Grade/CPN. namic properties). 2.1
Overall Architecture
Figure 2 shows the overall architecture of Grade/CPN. We see that we build on
top of Java and Access/CPN [
The central interface of Grade/CPN is PlugIn, shown in Listing 1 (ll. 1–5). Each plug-in must implement this interface. The configure method is a factory method to instantiate the plug-in, and takes how many points should be awarded if the plug-in succeeds and a configuration string. The format of the configuration string is defined by the plug-in, but will typically be a name identifying the plug-in and a list of named parameters. If the plug-in can be instantiated with a given configuration string, it returns a new configured instance and otherwise it returns null. This allows us to create an abstract factory for instantiating plugins from a string. Furthermore, a plug-in has a method grade, which is given a student ID, a base model (base), the student solution (model), and a connection to the simulator. The plug-in can use this information to arrive at its conclusion and return a Message, which comprises how many points are awarded and a descriptive message with the reason for the grade.
of Fig. 2 is responsible for emitting a report based on the result of the PlugIns.
All interfaced pertaining to reporting is shown in Listing 1 (ll. 7–17). The main class is Report (ll. 7–10), which is instantiated for each student ID and contains a set of pairs of PlugIns and Messages (produced by the grade method PlugIns). 1 public interface PlugIn { 2354 } ppuubblliicc MPleusgsIange cgornaf digeu( rSHetiu(gddheoLnuetbvIleDelSmiidma,uxPlPaoteiontrrtsiNs, iemtS utbrliaanstgeor, c) P;one tfirgiNu reat t imoond)e;l , 1111111112340567987 }}}pppuuuvppppbbbouuuullliiiibbbbdccclllliiiiccccacccdlllaaaMRdDDsssReeeessspesttpsoaaMRaDroiigtllreeee(((tpstS((SSsoadPatttriugtorrllduiieunn{{egbggn{IlnetIhhDppeeaalouddsi ngieedrritns),, ,, J{SCMStrot.eimr.sni.spngaog}g.ne.e.mnrteedscsseoautmglaetpi),losn{)Dene{t.t).a..i{.l }.. .. }.. . d}e t a i l s ) { . . . } 2222222222167895341029 }}}pppuuupppppbbbuuuuullliiibbbbbcccllllliiiiicccccaccbllaaaTLTCsssbtieeosssrsssntatttf<crTeCSiatRrgueoc(ueisnttTcptrfeelaoiear(LgrtstsPiuti>os{sSrltnuau<TgTttiPIetieeoneslssnutttgTmSs(SIu)uueanisiit>t{tttceeeSh(g,eu.{reF.i.t)tLiePlie{}sltue<xgc. StIo.en.tnnusfdd}i(ges)nu;tTrIaDets>itoSniudFistie,l e {)Pe{tri.N. .et } base ) { . . . }
A Message (ll. 11–13) ties together a number of awarded points, a descriptive message and a list of Details providing in-depth reasoning leading to the outcome. Each Detail (ll. 14–17) consists of a descriptive header and either a list of textual details or a single graphical component, which is rendered as an image in the resulting report. For each student a report overview is generated (see Fig. 3 for an example) and supplementary details are added in separate sections. Configuration. The Configuration component of Fig. 2 is shown in Listing 1 (ll. 19–29). The main class is a Tester (ll. 19–22), which given a TestSuite, a list of student IDs, and a base model can perform a test (l. 21) and yields a Report for each student. A TestSuite (ll. 23–26) has a distinguished matcher, which is a PlugIn mapping models to student IDs by yielding a high score for a model and student ID pair if the model is created by the student with the given ID and a low score otherwise. A TestSuite can also return a list of PlugIns for the main grading process. One implementation of a TestSuite, the ConfigurationTestSuite (ll. 27–29), is instantiated using a configurationFile which along with an abstract PlugIn factory is used to instantiate the correct PlugIns according to the configuration.
An example configuration file is shown in Listing 2. The file comprises two sections, matcher (ll. 1–2) and test (ll. 4–15), setting up the matcher and the actual tests graded, respectively. The intuition is that each line corresponds to a plug-in; a line starting with a + (ignoring white space) is considered part of the preceding line. Each line starts with a number indicating how many points are awarded for successful execution. If the number is negative, successful execution yields 0 points but a failure yields a punishment. This is followed by a colon and a configuration option recognized by the plug-in and optionally a list of named parameters. For example, in line 5 we see that the plug-in identified by declaration-preservation is instantiated with one named parameter. If the test fails, it yields a punishment of 5 points and if it succeeds, it yields 0 points. Lines 13– 14 are merged (as line 14 starts with +). In the following we go into more detail with this example. 2.2
Simple Plug-ins for Interface Preservation In Listing 2, we use two plug-ins to ensure that the interface to the environment and the environment itself are not modified. The declaration-preservation plug
1 [ matcher ] 2 −5: signature , threshold=65 4 [ tests ] 111110123498765 −−−00..551+++++00::0330([md((33[:((11−|−::ea00iRc−−tnbblce>>a∗∗ttthjerllef((arHicR,,−−lfttrraee−−aiee|nnjoc>>ppedane+ceelm−−eOtRaa_epp)tt|ressORdrrc===eeeeef>srsitf22veee)u,,nnrerrrf−aavnva)| mm>aa)i−+ltteeu>=(i==i−oo>r""|−nn(eOAA−>),fncc−aaccl>&ydOleespdpretRttpdw|]aeeo1rgc<0)eesci==vOa3>erf]ras)dlfes=aore>sif l",uicf,nraatieepitls)amutc=&raietryk)=&1tr"u,et e, ssut=bset=d e l i v e r y s e r v i c e in (l. 5) makes sure that no declaration in the provided model is removed or changed. This ensures that it is impossible to change the type of the interface by redefining color sets. If declarations are removed or changed, this is reported as an error and if new declarations are added, they are added to the report so it is easy to see what was added without having to compare the student model with the base model manually.
The interface-preservation (l. 6) plug-in makes sure that students do not change the given net structure, but only add new structure. In our example from Fig. 1, students are only allowed to add new net structure, but not to modify the given environment. Here, we are given four parameters. The addpages parameter is set to false, which means that students are not allowed to add new pages. The model used here is flat, and thus introducing hierarchy is considered an error. The initmark option is set to true, which means that students are not allowed to change the initial marking of the model. Finally, the subset parameter contains a list of pages students are allowed to add structure to. Any page not in this list is not allowed to be changed at all. Here, we specify that the students are allowed to alter the deliveryservice page from Fig. 1. Any added page is listed in the report as is any modified page. If the change is illegal, the error is listed (i.e., if a node of the interface is removed or altered, this is highlighted), and if the model contains no errors, the entire environment is dimmed so only the student solution is highlighted. 2.3
Fraud Prevention We have two plug-ins for matching a model to a student ID. In Listing 2, we use both to award points. We see in line 8 that we instantiate the matchfilename plugin. This plug-in simply checks if the student ID is a substring of the filename (and punishes if it is not). This is fine for honest students; unfortunately, we have in earlier years encountered students copying models from one another. To catch that, we instead use the more elaborate signature plug-in as matcher (l. 2).
The signature matcher exploits that all elements of a CPN Tools model have a unique identifier. This is necessary, e.g., to represent that an arc is connected to a specific place and transition. While these identifiers must be unique in the file and match for nodes and arcs, the actual contents of the identifiers have no semantics. We have developed a simple signer application which, given a base model, modifies the identifiers in a predictable way. By using a cryptographic random number generator, we can generate a sequence of pseudo-random numbers using the student ID and a secret passphrase as seed. The idea is that if we know the passphrase and the student ID, we can regenerate the sequence, but using just the sequence (and optionally the student ID), it is not possible to reverse-engineer the passphrase. Now, using the generated sequence of numbers as identifiers of model elements in the file containing the environment, we create a unique signature in the base file for each student.
The signature plug-in can check this signature. It queries for each student ID and student model whether the two match. It regenerates the sequence of random numbers for the student ID and the provided passphrase, and check that the identifiers are present in the file. If they are, the model is considered a match and otherwise not. The plug-in takes a parameter threshold which indicates how many identifiers must be present in the model. As the signing is a one-way process, students are forced to use the appropriate base model and cannot just hand in the same model (even after making cosmetic changes). 3
An important requirement to our tool is to check dynamic properties, requirement 4(b) from the introduction. In the example in Fig. 1, we are for example interested in the behavior when a customer accepts packets ten times in a row and how many packets can be outstanding at any time. As CPN models tend to have huge or even infinite state spaces, we cannot verify such properties in general and especially not for models generated by students who have less experience with modeling. Therefore, we check such properties by guiding the simulator; that is, we apply a testing-based approach rather than exhaustive state-space exploration, yielding a sound but not necessarily complete checking mechanism.
Guiding the simulator requires to specify which transition the simulator
should execute. Testing whether some property holds in a state of the model
requires a specification of this property. To this end, we introduce the Britney
Temporal Logic (BTL). This logic is similar to linear-time logic (LTL) [
Syntax A BTL formula is a hguidei. A guide describes how simulation should be performed; that is, it guides the simulator to a desired state. The atomic propositions of a guide are described using hsimplei, which is an expression without temporal operators but otherwise allowing full propositional logic on transitions and place invariants. The temporal operators are various arrows emulating the arrows typically used to describe transition steps. Thus a->b means that first a must hold and subsequently b must hold. For example, a and b can represent transitions, meaning that for the formula to hold, the corresponding transitions are executed one after the other. We lift this operator to a-->b meaning that a must hold and at some point afterward b must hold. Finally, a--->[b] means that a must hold and when the simulation stops b must hold. The brackets indicate that b is not used for guiding the simulation anymore (it has terminated after all). We hguidei :=-can omit a, which is an abbreviation for true. For each kind of arrow, we also add a double arrow version indicating that if a holds, then b just holds at the appropriate time. We also allow bounded and unbounded repetition using a star syntax. In contrary to a regular Kleene star, we put it in front as it improves readability for western readers. We allow conjunctions of guides using &, but no disjunctions because for an expression like (a->b)|(c->d) it is not obvious whether to guide the simulation with an a or a c if both are enabled (as we do not know whether b or d are enabled in the next step).
A guide can also include hcheck is, which are not used to guide the simulator but only to test assertions. They are therefore allowed to contain disjunctions and negations and general boolean expressions. Finally, a guide can include the special keyword ‘failure’, which is a synonym for ‘false’ but with a very restricted syntax. This means that we try to stay clear of transitions that would violate the formula. The BTL formula in Listing 2 (ll. 8-12) guides a model to execute a transition Order exactly 10 times (l. 9) and a transition Receive exactly 10 times (l. 10) with any intermediate transitions allowed except for Reject (l. 11). hguidei hguidei hsimplei ‘->’ hguidei ‘-->’ hguidei hcheck i ::=-hsimplei ::=-hguidei
‘--->’ ‘[’ hcheck i ‘]’ hguidei ‘=>’ hguidei hguidei ‘==>’ hguidei hguidei ‘===>’ ‘[’ hcheck i ‘]’ hnumber i ‘*’ hguidei
‘*’ hsimplei ‘[’ hcheck i ‘]’ ‘(’ ‘-->’ hsimplei ‘)’ ‘=>’ ‘failure’ hguidei ‘&’ hguidei
‘(’ hguidei ‘)’ hguidei hguidei ‘|’ hguidei ‘!’ hguidei
hbexpi ‘(’ hcheck i ‘)’ hnamei ‘true’ ‘false’ ‘!’ hsimplei hsimplei ‘&’ hsimplei hsimplei ‘|’ hsimplei ‘(’ hsimplei ‘)’
In addition to the syntax for guiding, we also allow boolean expressions. These are mostly for testing state properties, such as counting the tokens on a place or testing values of the global clock. Boolean expression are defined in the standard way and shall not be repeated here due to space limitations. Line 12 in Listing 2 tests that Handle Return is never executed (but does not enforce it like the guides). The formula in line 14 checks that at any point during execution, the three places Reject, Offer, and Accept never contain 3 or more tokens in total. 3.2
Semantics
We interpret formulae specified in BTL over the state space of a CPN. The state
space of a CPN can be seen as a Kripke structure K = (Q, δ, q0, Σ, λ), where
Q is a set of states, q0 ∈ Q is the initial state, Σ is a set of transition labels,
δ ⊆ Q × Σ × Q is the transition relation, and function λ : Q →− 2AP maps each
state q ∈ Q to a set of atomic propositions that hold in q. As usual, AP denotes
the set of all atomic propositions. As BTL is an LTL-like logic, we also introduce
the notion of a trace. A trace is a transition sequence q0, . . . , qk such that q0 is
the initial state and for all 0 ≤ i < k, there exists an a ∈ Σ with (qi, a, qi+1) ∈ δ.
The semantics is similar to a standard finite trace semantics for LTL like the
one defined in [
Our syntax includes a lot of conveniences. We already mentioned that avoiding the precondition for the single-arrows is a convenience for a precondition of true and that ‘failure’ is semantically the same as ‘false’. Furthermore, all single arrows can be defined from the double arrows by forcing the precondition. The eventuality defined by a==>b can be defined in terms of the unbounded repetition and the next operator, and bounded repetition is just a syntactical convenience:
->G ≡ true->G -->G ≡ true-->G --->[B] ≡ true--->[B]
failure ≡ false
G1->G2 ≡ G1&G1=>G2 G1-->G2 ≡ G1&G1==>G2 G--->[B] ≡ G&G===>[B] G1==>G2 ≡ G1->(∗true->G2)
(G->(n − 1) ∗ (G) n ∗ (G) ≡ true if n ≥ 1 otherwise.
The semantics of hsimplei can now be defined over the traces of a Kripke structure K. Attribute name in the grammar thereby refers to a transition label. – Every trace (q0, . . . , qk) satisfies (q0, . . . , qk) |= true and (q0, . . . , qk) 6|= false. – (q0, q1, . . . , qk) |= name iff q0 −n−a−m→e q1. – (q0, q1, . . . , qk) |=!S iff (q0, q1, . . . , qk) 6|= S.
– (q0, q1, . . . , qk) |= S1&S2 iff (q0, q1, . . . , qk) |= S1 ∧ (q0, q1, . . . , qk) |= S2. – (q0, q1, . . . , qk) |= S1|S2 iff (q0, q1, . . . , qk) |= S1 ∨ (q0, q1, . . . , qk) |= S2.
Boolean expressions can be evaluated over the set AP of atomic propositions and are, therefore, evaluated at a state. The remaining operators are LTLlike and are therefore defined over traces. We write q0 −G→ qk to denote that (q0, . . . , qk) |= G. The first is unbounded repetition. We notice that this is satisfied regardless of what we do (as zero repetitions can be performed).
Operator => is similar to the next operator in LTL (though here it is conditional): If G1 holds on a trace q0, . . . , qj then G2 must hold starting from qj . – guide(∗G) = T , – guide(q, G1=>G2) = T , – guide(q, [B]) = T , – guide(q, G===>[B]) = T , – guide(q, [G]) = T , q −G→ q00, q00 −(−‘*−’−G→) q0 q −(−‘*−’−G→) q0 ,
q −(−‘*−’−G→) q0 q0 −G−→1 qj =⇒ qj −G−→2 qk, 0 < j < k q0 −G−1−=−>G−→2 qk (1) (2) (3) (4)
The following three rules define operators used for checking a property (expressed by putting the expression into squared brackets). We use them to check whether a boolean expression holds, a boolean expression holds in a final state after guiding the simulator using expression G, and whether a guide holds. q0 |= B q0 −[−B→] qk ,
qk |= B q0 −G−−==−=−>[−B→] qk ,
G ∀j ≤ k : ¬(q0 −→ qj ) , q0 −G−−==−=−>[−B→] qk
G q0 −→ qk q0 −[−G→] qk
q0 −G−→1 qk ∧ q0 −G−→2 qk
q0 −G−−1&−G−→2 qk
The final consideration is how we guide. This is done by defining a set of allowed transitions for each guide. For simulation, only transitions that are in this set are considered. This in particular means that if the set of allowed transitions is empty, the simulation is considered finished (and not with an error unless the formula is not satisfied). We define the set guide over a set T of possible transitions inductively as: – guide(q, S) = {name ∈ T | q −n−a−m→e q0 =⇒ (q, q0) |= S},
(guide(G) if n ≥ 1, – guide(q, n‘*’G)
T otherwise,
We more or less just allow concrete steps if they are needed to satisfy a formula or forbid a step if it would violate a formula, and otherwise allow anything when we do not care about the outcome. 3.3
Implementation Our implementation of BTL uses simple formula rewriting. Our implementation implements the guide set for filtering enabled transitions, pick and execute one that is in the guide set and in the set of enabled transitions. We then rewrite the formula according to the previous rules. For efficiency, we have expanded some of the syntactical equivalences, most importantly the future temporal operator (a==>b). When no more transitions are in the intersection, we check if the rewritten formula is satisfied for the empty trace.
We evaluate formulae
using a four-value logic similar
to [
In addition to the grader used by teachers to finally grade assignments, we also have two tools for testing BTL formulas. One is used during construction to help a teacher get immediate feedback on a formula and a solution by manually or experimentally testing formulas on a proposed solution. A simplified version of this tool allows students to check that their models conform to the formulas. This tool also allows students to manually single-step through their model and watch the formula progress, aiding in finding and avoiding obvious errors before handing in.
In this section, we present first experiences we made with Grade/CPN in supporting the evaluation of a CPN assignment in the course Business Information Systems at the Eindhoven University of Technology. In this assignment, students were given the base model in Fig. 1 and they had to model the delivery system according to a textual specification. Each of the 94 students had to submit two models. We received in total 130 models from 66 students.
In a first step of the assessment, we applied Grade/CPN by calling it with a student model, the base model, and a configuration file (see Listing 2). Here, we were interested whether the interface and declaration of the base model have been preserved, whether there is a suspicion of fraud, and whether six scenarios can be replayed on the model (only two are shown in the Listing). The scenarios were part of the specification of the assignment, and we specified them using BTL. As BTL refers to the interface, it is crucial that students have not changed it. The runtime of the tool was about ten minutes for all students; that is, after this time, a report had been generated for each student. The tool detected two fraud attempts, though they turned out to be caused by students handing in a subsequent assignment using the same base model as well.
In a second step, we manually checked each of the generated reports. On average, this took less than five minutes for each report. Based on the feedback provided by Grade/CPN, it was easy to check whether a model was actually correct or not. Basically, the violation of a certain scenario simplified the detection of the cause for this violation drastically. In most cases, we did not even have to look at the counterexample provided by our tool. Overall, we had to simulate only five models manually to determine the cause of an error. The tool automatically detected several subtle errors such as wrong guards and minor changes to the environment without having the need to open the respective model; it is highly unlikely we would have caught all of these completely manually. We even found subtle errors in our own solutions, yielding better results.
Based on experience from previous years, the use of Grade/CPN reduced the amount of time for grading the assignment by a factor of at least two to three. This is factoring in that we used Grade/CPN for the first time and had to both define and understand the defined logic BTL, and also did not place complete confidence in the reported results which probably increased the manual labor as well. As correcting models is a rather monotonous work, it is easily possible that one oversees an error or forgets to check some scenario. Using Grade/CPN, this is now impossible and, therefore, we think that we can provide students with a fairer (in the sense of more equal) grading on the one hand and better feedback on the other hand. 5
We have presented Grade/CPN, a tool to semi-automatically grade CPN models. Using Access/CPN, we can support any model created using CPN Tools. The plug-in architecture makes the tool easily extendible: to do so, one must just implement the interface in Listing 1 (ll. 1–5). The pluggable configuration with a very simple base format makes configuration simple. Configuration comprises selecting which plug-ins to use, which weight to assign them, and which parameters to instantiate them. Each plug-in only needs to consider its own options as the overall configuration format is handled by Grade/CPN. Reporting is handled by making all plug-ins return simple messages optionally annotated with more detailed reasoning (Listing 1 ll. 13–15). The information is automatically gathered by Grade/CPN and presented both as an overview in the user interface and as a detailed report. We have presented both simple plug-ins and a very powerful one implementing guided checking of Britney Temporal Logic (BTL). BTL allows us to guide the simulation toward desired scenarios and to check that the environment contracts are adhered to. All plug-ins provide categorized information explaining the score and highlighting any changes made to the model, so teachers processing the reports only have to focus on things that cannot be automatically checked. We have designed and implemented an infrastructure for detecting fraud. We have reported on our experience with the Business Information Systems course where Grade/CPN was used to grade 130 assignments from 66 students. Using Grade/CPN instead of a completely manual approach reduced the manual labor by a factor of three. Each student has to hand in a total of five models during the course, so anticipated time savings are immense.
The idea of (semi-)automatically grading assignments is not new and closely
related to testing. A known testing framework is JUnit [
Future work includes loosening what is allowed in guides by having the tool try resolving, e.g., disjunctions itself (by keeping track of which branches have been explored and only reporting errors if no branch is successful). We also consider a designer for automatically building BTL formulae and full configuration files by manually guiding the simulation in a manner similar to our current tool for testing BTL formulas. We aim to integrate Grade/CPN with Jenkins or peach3 so we can combine our simplicity of configuration with the more advanced features of those systems. While BTL is designed for grading assignments using testing, it has also proved useful for finding errors in our model. It would be interesting to investigate this further, including making testing complete by exploiting the guiding perspective of our logic.
Acknowledgements. The authors thank Boudewijn van Dongen for fruitful discussions about the requirements for an automatic grader.