We present a pattern system for property specification. It extends the existing patterns identified in [4] which allow to reason about occurrence and order of events, but not about time conditions. Introducing time-related patterns allows the specification of real-time requirements. The paper is limited to 3 pages. Therefore it contains only basic ideas. The details can be found in [9].

The correctness of a workflow specification is critical for the automation of business processes. For this reason, errors in the specification should be detected and corrected as early as possible - at specification time. In this paper, we present a validation method for workflow specifications using model-checking techniques. A formalized workflow specification, its properties and the correctness requirements are translated into a timed state machine that can be analyzed with the Uppaal model checker. The main contribution of this paper is the use of timed model checking for verifying time-related properties of workflow specifications. Using only one tool (the model checker) for verifying these different kinds of properties gives an advantage over using different specialized algorithms for verifying different kinds of properties.

Since 2009, Moving Target Defense (MTD) has become a new paradigm of defensive mechanism that frequently changes the state of the target system to confuse the attacker. This frequent change is costly and leads to a trade-off between misleading the attacker and disrupting the quality of service. Optimizing the MTD activation frequency is necessary to develop this defense mechanism when facing realistic, multi-step attack scenarios. Attack modeling formalisms based on DAG are prominently used to specify these scenarios. It represents the attack goal in the root of a tree that is recursively refined into subgoals to show the different ways the attacker can compromise the system. According to some specific models, the tree is augmented with countermeasures, time, costs, or probabilities. Our contribution is a new DAG-based formalism for MTDs and its translation into a Price Timed Markov Decision Process to find the best activation frequencies against the attacker’s time/cost-optimal strategies. For the first time, MTD activation frequencies are analyzed in a state-of-the-art DAG-based representation. Moreover, this is the first paper that considers the specificity of MTDs in the automatic analysis of attack modeling formalisms. Finally, we present some experimental results using UPPAAL STRATEGO to demonstrate its applicability and relevance. / Sedan 2009 har Moving Target Defense (MTD) blivit ett nytt paradigm av defensiv mekanism som ofta ändrar målsystemets tillstånd för att förvirra angriparen. Denna frekventa förändring är kostsam och leder till en avvägning mellan att vilseleda angriparen och att störa målsystemets tillförlitlighet. Att optimera MTD-aktiveringsfrekvensen är nödvändigt för att utveckla denna försvarsmekanism när man står inför realistiska attackscenarier i flera steg. Attackmodelleringsformalismer baserade på DAG är de främst använda metoderna för att specificera dessa scenarier. Metoden representer attackmålet i roten av ett träd som rekursivt förfinas till delmål för att visa de olika sätt som angriparen kan äventyra systemet. Enligt vissa specifika modeller är trädet utökat med motåtgärder, tid, kostnader eller sannolikheter. Vårt bidrag är en ny DAG-baserad formalism för MTD:er och dess översättning till en Price Timed Markov Decision Process för att hitta de bästa aktiveringsfrekvenserna mot angriparens tids-/kostnadsoptimala strategier. För första gången analyseras MTD-aktiveringsfrekvenser i en toppmodern DAG-baserad representation. Dessutom är detta det första rapporten som överväger specificiteten hos MTD:er i den automatiska analysen av attackmodelleringsformalismer. Slutligen presenterar vi några experimentella resultat med UPPAAL STRATEGO för att visa dess tillämpbarhet och relevans.