Designing secure business processes with SecBPMN

Modern information systems are increasingly large and consist of an interplay of technical components and social actors (humans and organizations). Such interplay threatens the security of the overall system and calls for verification techniques that enable determining compliance with security policies. Existing verification frameworks either have a limited expressiveness that inhibits the specification of real-world requirements or rely on formal languages that are difficult to use for most analysts. In this paper, we overcome the limitations of existing approaches by presenting the SecBPMN framework. Our proposal includes: (1) the SecBPMN-ml modeling language, a security-oriented extension of BPMN for specifying composite information systems; (2) the SecBPMN-Q query language for representing security policies; and (3) a query engine that enables checking SecBPMN-Q policies against SecBPMN-ml specifications. We evaluate our approach by studying its understandability and perceived complexity with experts, running scalability analysis of the query engine, and through an application to a large case study concerning air traffic management.     

Practical verification of decision-making in agent-based autonomous systems

We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.     

Modelling socio-ecological systems with MAIA: A biogas infrastructure simulation

Similar to other renewable energy technologies, the development of a biogas infrastructure in the Netherlands is going through social, institutional and ecological evolution. To study this complex evolutionary process, we built a comprehensive agent-based model of this infrastructure. We used an agent-based modelling framework called MAIA to build this model with the initial motivation that it facilitates modelling complex institutional structures. The modelling experience however proved that MAIA can also act as an integrated solution to address other major modelling challenges identified in the literature for modelling evolving socio-ecological systems. Building on comprehensive reviews, we reflect on our modelling experience and address four key challenges of modelling evolving socio-ecological systems using agents: (1) design and parameterization of models of agent behaviour and decision-making, (2) system representation in the social and spatial dimension, (3) integration of socio-demographic, ecological, and biophysical models, (4) verification, validation and sensitivity analysis of such ABMs.     

Consistency preserving co-evolution of formal specifications and agent-oriented conceptual models

Many modelling techniques tend to address “late-phase” requirements while many critical modelling decisions (such as determining the main goals of the system, how the stakeholders depend on each other, and what alternatives exist) are taken during early-phase requirements engineering. The i¹ modelling framework is a semiformal agent-oriented conceptual modelling language that is well-suited for answering these questions. This paper addresses key challenge faced in the practical deployment of agent-oriented conceptual modelling frameworks such as i¹. Our approach to addressing this problem is based on the observation that the value of conceptual modelling in the i¹ framework lies in its use as a notation complementary to existing requirements modelling and specification languages, i.e., the expressive power of i¹ complements rather than supplants that of existing notations. The use of i¹ in this fashion requires that we define methodologies that support the co-evolution of i¹ models with more traditional specifications. This research examines how this might be done with formal specification notations (specifically Z).     

A logic of argumentation for specification and verification of abstract argumentation frameworks

In this paper, we propose a logic of argumentation for the specification and verification (LA4SV) of requirements on Dung??s abstract argumentation frameworks. We distinguish three kinds of decision problems for argumentation verification, called extension verification, framework verification, and specification verification respectively. For example, given a political requirement like ??if the argument to increase taxes is accepted, then the argument to increase services must be accepted too,?? we can either verify an extension of acceptable arguments, or all extensions of an argumentation framework, or all extensions of all argumentation frameworks satisfying a framework specification. We introduce the logic of argumentation verification to specify such requirements, and we represent the three verification problems of argumentation as model checking and theorem proving properties of the logic. Moreover, we recast the logic of argumentation verification in a modal framework, in order to express multiple extensions, and properties like transitivity and reflexivity of the attack relation. Finally, we introduce a logic of meta-argumentation where abstract argumentation is used to reason about abstract argumentation itself. We define the logic of meta-argumentation using the fibring methodology in such a way to represent attack relations not only among arguments but also among attacks. We show how to use this logic to verify the requirements of argumentation frameworks where higher-order attacks are allowed [A preliminary version of the logic of argumentation compliance was called the logic of abstract argumentation?(2005).]     

Formal enforcement and management of obligation policies

Obligations are generally actions that users are required to take and are essential for the expression of a large number of requirements. For instance, obligation actions may represent prerequisites to gain some privilege (pre obligations), to satisfy some ongoing or post requirement for resource usage (ongoing and post obligations), or to adhere to some privacy or availability policy. Obligations may also define states of affairs which should be maintained. An example of such obligations is the obligation “doctors should remain alert while in the operating room”. In this paper, we introduce a formal framework for the management and enforcement of obligation policies. The framework is formalized using concepts from action specification languages and the Event Condition Action paradigm of active databases. Therefore, our framework allows reasoning about change in the state of obligations and, at the same time, provides declarative formal semantics for their enforcement. In this framework, we support many types of obligations and show how to manage obligation activation, fulfillment and violation.     

Concurrent software verification with states, events, and deadlocks

We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification. We also present an algorithm to detect deadlocks in concurrent message-passing programs. Deadlock- freedom is not only an important and desirable property in its own right, but is also a prerequisite for the soundness of our model checking algorithm. Even though deadlock is inherently non-compositional and is not preserved by classical abstractions, our iterative algorithm employs both (non-standard) abstractions and compositional reasoning to alleviate the state-space explosion problem. The resulting framework differs in key respects from other instances of the counterexample-guided abstraction refinement paradigm found in the literature. We have implemented this work in the magic verification tool for concurrent C programs and performed tests on a broad set of benchmarks. Our experiments show that this new approach not only eases the writing of specifications, but also yields important gains both in space and in time during verification. In certain cases, we even encountered specifications that could not be verified using traditional pure event-based or state-based approaches, but became tractable within our state/event framework. We also recorded substantial reductions in time and memory consumption when performing deadlock-freedom checks with our new abstractions. Finally, we report two bugs (including a deadlock) in the source code of Micro-C/OS versions 2.0 and 2.7, which we discovered during our experiments. This research was sponsored by the National Science Foundation (NSF) under grants no. CCR-9803774 and CCR-0121547, the Office of Naval Research (ONR) and the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796, the Army Research Office (ARO) under contract no. DAAD19-01-1-0485, and was conducted as part of the Predictable Assembly from Certifiable Components (PACC) project at the Software Engineering Institute (SEI). This article combines and builds upon the papers (CCO⁺04) and (CCOS04). Received December 2004 Revised July 2005 Accepted July 2005 by Eerke A. Boiten, John Derrick, Graeme Smith and Ian Hayes     

A real-time profile for UML

This paper describes an approach for real-time modelling in UML, focusing on analysis and verification of time and scheduling-related properties. To this aim, a concrete UML profile, called the ωprofile, is defined, dedicated to real-time modelling by identifying a set of relevant concepts for real-time modelling which can be considered as a refinement of the standard SPT profile. The profile is based on a rich concept of event representing an instant of state change, and allows the expression of duration constraints between occurrences of events. These constraints can be provided in the form of OCL-like expressions annotating the specification or by means of state machines, stereotyped as ‘observers’. A framework for modelling scheduling issues is obtained by adding a notion of resource and a notion of execution time. For proving the relevance of these choices, the profile has been implemented in a validation tool and applied to case studies. It has a formal semantics and is sufficiently general and expressive to define a semantic underpinning for other real-time profiles of UML which in general define more restricted frameworks. In particular, most existing profiles handling real-time issues define a number of predefined attributes representing particular durations or constraints on them and their semantic interpretation can be expressed in the OMEGA-RT profile. This work has been partially supported by the IST-2002-33522 OMEGA project. VERIMAG is an academic research laboratory associated with CNRS, Université Joseph Fourier and Institut Nationale Polytechnique de Grenoble.     

基于Petri网的RBAC策略验证的研究

本文为RBAC模型提出了一个基于着色Petri网的策略规格说明和分析的架构．Petri网能够捕获基数、责任分离等约束，而且能对优先和依赖约束进行说明、使用Petri网的可达到性分析技术对RBAC策略进行正确性验证．     

Behavioural equivalence in simulation modelling

Discrete event simulation has grown up as a practical technique for estimating the quantitative behaviour of systems, where direct measurement is undesirable or impractical. It is also used to understand the detailed functional behaviour of such systems. Its theory is largely that of experimental science, centering on statistical approaches to validation, rather than on the verification of detailed behaviour. On the other hand, much work has been done on understanding and proving functional properties of systems, using techniques of formal specification and concurrency modelling. This article presents an approach to understanding equivalence of behaviour of discrete event simulation models, using a technique from the concurrency world, Milner’s Calculus of Communicating Systems (CCS). This yields a significant advance over the main previous work, Schruben and Yücesan’s simulation graphs. CCS allows for the use of observational equivalence, which can capture a more flexible, behavioural notion of equivalence than the structural equivalence defined there.A common framework based on the process view of models is constructed, using a hierarchical graphical modelling language (Extended Activity Diagrams). This language is shown to map onto both the major constructs of the DEMOS discrete event simulation language and the corresponding CCS models. A graphically driven tool based on such a framework is presented, which generates both types of models. Using the CCS model, behavioural equivalences and differences in simulation models are demonstrated.     

Electronic institutions for B2B: dynamic normative environments

The regulation of the activity of multiple autonomous entities represented in a multi-agent system, in environments with no central design (and thus with no cooperative assumption), is gaining much attention in the research community. Approaches to this concern include the use of norms in so-called normative multi-agent systems and the development of electronic institution frameworks. In this paper we describe our approach towards the development of an electronic institution providing an enforceable normative environment. Within this environment, institutional services are provided that assist agents in forming cooperative structures whose commitments are made explicit through contracts. Our normative framework borrows some concepts from contract law theory. Contracts are formalized using norms which are used by the institution while monitoring agents’ activities, thus making our normative environment dynamic. We regard the electronic institution as a means to facilitate both the creation and the enforcement of contracts between agents. A model of “institutional reality” is presented that allows for monitoring the fulfillment of norms. The paper also distinguishes our approach from other developments of the electronic institution concept. We address the application of our proposal in the B2B field, namely regarding the formation of Virtual Organizations.     

Interactive specification and verification of behavioral adaptation contracts

ContextAdaptation is a crucial issue when building new applications by reusing existing software services which were not initially designed to interoperate with each other. Adaptation contracts describe composition constraints and adaptation requirements among these services. The writing of this specification by a designer is a difficult and error-prone task, especially when interaction protocols are considered in service interfaces.ObjectiveIn this article, we propose a tool-based, interactive approach to support the contract design process.MethodOur approach includes: (i) a graphical notation to define port bindings, and an interface compatibility measure to compare protocols and suggest some port connections to the designer, (ii) compositional and hierarchical techniques to facilitate the specification of adaptation contracts by building them incrementally, (iii) validation and verification techniques to check that the contract will make the involved services work correctly and as expected by the designer.ResultsOur results show a reduction both in the amount of effort that the designer has to put into building the contract, as well as in the number of errors present in the final result (noticeably higher in the case of manual specification).ConclusionWe conclude that it is important to provide integrated tool support for the specification and verification of adaptation contracts, since their incorrect specification induces erroneous executions of the system. To the best of our knowledge, such tool support has not been provided by any other approach so far, and hence we consider the techniques described in this paper as an important contribution to the area of behavioral software adaptation.     

Hybrid

Combining higher-order abstract syntax and (co)-induction in a logical framework is well known to be problematic. We describe the theory and the practice of a tool called Hybrid, within Isabelle/HOL and Coq, which aims to address many of these difficulties. It allows object logics to be represented using higher-order abstract syntax, and reasoned about using tactical theorem proving and principles of (co)induction. Moreover, it is definitional, which guarantees consistency within a classical type theory. The idea is to have a de Bruijn representation of λ-terms providing a definitional layer that allows the user to represent object languages using higher-order abstract syntax, while offering tools for reasoning about them at the higher level. In this paper we describe how to use Hybrid in a multi-level reasoning fashion, similar in spirit to other systems such as Twelf and Abella. By explicitly referencing provability in a middle layer called a specification logic, we solve the problem of reasoning by (co)induction in the presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications of object logic inference rules. We first demonstrate the method on a simple example, formally proving type soundness (subject reduction) for a fragment of a pure functional language, using a minimal intuitionistic logic as the specification logic. We then prove an analogous result for a continuation-machine presentation of the operational semantics of the same language, encoded this time in an ordered linear logic that serves as the specification layer. This example demonstrates the ease with which we can incorporate new specification logics, and also illustrates a significantly more complex object logic whose encoding is elegantly expressed using features of the new specification logic.     

A declarative two-level framework to specify and verify workflow and authorization policies in service-oriented architectures

The specification of distributed service-oriented applications spans several levels of abstraction, e.g., the protocol for exchanging messages, the set of interface functionalities, the types of the manipulated data, the workflow, the access policy, etc. Many (even executable) specification languages are available to describe each level in separation. However, these levels may interact in subtle ways (for example, the control flow may depend on the values of some data variables) so that a precise abstraction of the application amounts to more than the sum of its per level components. This problem is even more acute in the design phase when automated analysis techniques may greatly help the difficult task of building “correct” applications faced by designers. To alleviate this kind of problems, this paper introduces a framework for the formal specification and automated analysis of distributed service-oriented applications in two levels: one for the workflow and one for the authorization policies. The former allows one to precisely describe the control and data parts of an application with their mutual dependencies. The latter focuses on the specification of the criteria for granting or denying third-party applications the possibility to access shared resources or to execute certain interface functionalities. These levels can be seen as abstractions of one or of several levels of specification mentioned above. The novelty of our proposal is the possibility to unambiguously specify the—often subtle—interplay between the workflow and policy levels uniformly in the same framework. Additionally, our framework allows us to define and investigate verification problems for service-oriented applications (such as executability and invariant checking) and give sufficient conditions for their decidability. These results are non-trivial because their scope of applicability goes well beyond the case of finite state spaces allowing for applications manipulating variables ranging over infinite domains. As proof of concept, we show the suitability and flexibility of our approach on two quite different examples inspired by industrial case studies.     

Temporal logic programming for assembly sequence planning

A temporal-constraint logic programming framework for the specification and automatic verification and synthesis of assembly sequences is developed. The implemented tool is based on the formulated and derived precedence properties for a general mechanical assembly. This tool, called the Mechanical Assembly Sequence Satisfiability Checker (MASS-C), supports the use of a subset of temporal logic for assembly constraint specification. MASS-C provides the logic programming framework by which the designer can be relieved of the tedium of finding the assembly sequences, and the assembly sequence planning process manifests itself in the implicit modelling of assembly sequences by acquiring and formulating the set of correct and complete assembly constraints as a logic program. MASS-C implements a class of temporal expressions as predicates for logic programming of assembly constraints. It provides facilities to either verify an assembly sequence or synthesise all assembly sequences that satisfy the specified constraints composed as a logic program. Two examples illustrate the use of MASS-C for such verification and synthesis.     

Inter-domain policy violations in multi-hop overlay routes: Analysis and mitigation

The Internet is a complex structure arising from the interconnection of numerous autonomous systems (AS), each exercising its own administrative policies to reflect the commercial agreements behind the interconnection. However, routing in service overlay networks is quite capable of violating these policies to its advantage. To prevent these violations, we see an impending drive in the current Internet to detect and filter overlay traffic. In this paper, we first present results from a case study overlay network, constructed on top of PlanetLab, that helps us gain insights into the frequency and characteristics of the different inter-domain policy violations. Further, we investigate the impact of two types of overlay traffic filtering that aim to prevent these routing policy violations: blind filtering and policy-aware filtering. We show that such filtering can be detrimental to the performance of overlay routing. We next consider two approaches that allow the overlay network to realize the full advantage of overlay routing in this context. In the first approach, overlay nodes are added so that good overlay paths do not represent inter-domain policy violations. In the second approach, the overlay acquires permits from certain ASes that allow certain policy violations to occur. We develop a single cost-sharing framework that allows the incorporation of both approaches into a single strategy. We formulate and solve an optimization problem that aims to determine how the overlay network should allocate a given budget between paying for additional overlay nodes and paying for permits (transit and exit) to ASes. We illustrate the use of this approach on our case study overlay network and evaluate its performance under varying network characteristics.