Search

This paper ascribes a formal semantics to advice weaving in AspectJ. Since the version 1.1, AspectJ language is developed using bytecode weaving, which combines aspects and classes to produce ".class" files that run in a Java Virtual Machine (JVM). In AspectJ, advice weaving is done statically by inserting the advice functionality in some regions of the code. These regions are join points that are declared using pointcuts. In this paper, we focus only on static pointcuts, i.e., pointcuts that correspond directly to locations in the bytecode. AspectJ dynamic pointcuts such as target, this, and cflow are not in the focus of this paper. [ABSTRACT FROM AUTHOR]

The static determination of approximated values of string expressions has many potential applications. For instance, approximated string values may be used to check the validity and security of generated strings, as well as to collect the useful string properties. Previous string analysis efforts have been focused primarily on the maxmization of the precision of regular approximations of strings. These methods have not been completely satisfactory due to the difficulties in dealing with heap variables and context sensitivity. In this paper, we present an abstract-interpretation-based solution that employs a heuristic widening method. The presented solution is implemented and compared to JSA. In most cases, our solution gives results as precise as those produced by previous methods, and it makes the additional contribution of easily dealing with heap variables and context sensitivity in a very natural way. We anticipate the employment of our method in practical applications. [ABSTRACT FROM AUTHOR]

This paper tackles a problem often overlooked in functional programming community: that of testing. Fully automatic test tools like ${\sf{Quickcheck}}$ and ${\sf {G{\forall}ST}}$ can test first order functions successfully. Higher order functions, HOFs, are an essential and distinguishing part of functional languages. Testing HOFs automatically is still troublesome since it requires the generation of functions as test argument for the HOF to be tested. Also the functions that are the result of the higher order function needs to be identified. If a counter example is found, the generated and resulting functions should be printed, but that is impossible in most functional programming languages. Yet, bugs in HOFs do occur and are usually more subtle due to the high abstraction level. In this paper we present an effective and efficient technique to test higher order functions by using intermediate data types. Such a data type mimics and controls the structure of the function to be generated. A simple additional function transforms this data structure to the function needed. We use a continuation based parser library as main example of the tests. Our automatic testing method for HOFs reveals errors in the library that was used for a couple of years without problems. [ABSTRACT FROM AUTHOR]

Earlier work explored the introduction of session types into object oriented languages. Following the session types literature, two parties would start communicating, provided the types attached to that communication, i.e. the corresponding session types, were dual of each other. Then, the type system was able to ensure soundness, in the sense that two communicating partners were guaranteed to receive/send sequences of values following the order specified by their session types. In the current paper we improve upon our earlier work in two ways: we extend the type system to support bounded polymorphism, and we make the selection more object-oriented, so that control structures determine how to continue evaluation, depending on the class of the object being sent/received. Interestingly, although our notion of selection is more powerful than that in earlier work, the ensuing system turned out not to be more complex, except for the notion of duality, which needed to be extended, to correctly deal with bounded polymorphism, and to capture the new notion of selection. The paper contains an example, informal explanations, a formal description of the operational semantics and of type system, and a proof of subject reduction. [ABSTRACT FROM AUTHOR]

This paper addresses the problem of off-line selection of test cases for testing the conformance of a black-box implementation with respect to a specification, in the context of reactive systems. Efficient solutions to this problem have been proposed in the context of finite-state models, based on the ioco conformance testing theory. An extension of these is proposed in the context of infinite-state specifications, modelled as automata extended with variables. One considers the selection of test cases according to test purposes describing abstract scenarios that one wants to test. The selection of program test cases then consists in syntactical transformations of the specification model, using approximate analyses. [ABSTRACT FROM AUTHOR]

This paper provides a call-by-name and a call-by-value calculus, both of which have a Curry-Howard correspondence to the minimal normal logic K. The calculi are extensions of the λμ-calculi, and their semantics are given by CPS transformations into a calculus corresponding to the intuitionistic fragment of K. The duality between call-by-name and call-by-value with modalities is investigated in our calculi. [ABSTRACT FROM AUTHOR]

This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. These technical results establish the foundation of polymorphic delimited continuations. [ABSTRACT FROM AUTHOR]

A natural way to generate test cases for a Prolog program is to view the call patterns of the procedures in the program as an implicit representation of the control flow graph (CFG) of the program. This paper explores the idea by proposing a call patterns-based test case generation method, where a set of call patterns or computed answers is used to describe the paths in a CFG. With a constraint-based call patterns semantics, this method is formalized. Through the use of a proper constraints solver, we can generate test cases automatically from the sets of constraints. This method can be based on any approximation of the call patterns semantics. So compared with traditional CFG-based test case generation, the method is more flexible and can be easily adapted to meet the requirements of a tester expressed by the approximation of the call patterns semantics we use. [ABSTRACT FROM AUTHOR]

Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most undergraduates: e.g., assertions, pre- and postconditions, and invariants. Unfortunately, these constructs are not sufficiently expressive to permit formal modular verification of programs written in modern object-oriented languages like Java. The necessary extra constructs for specifying an object-oriented module include (perhaps the less familiar) frame properties, datagroups, and ghost and model fields. These constructs help specifiers deal with potential problems related to, for example, unexpected side effects, aliasing, class invariants, inheritance, and lack of information hiding. This tutorial paper focuses on JML's realization of these constructs, explaining their meaning while illustrating how they can be used to address the stated problems. [ABSTRACT FROM AUTHOR]

This paper is a survey of several techniques that have proven useful in establishing compatibility among behaviorally similar programs (e.g., system upgrades, object sub- and supertypes, system components produced by different vendors, etc.). We give a comparative analysis of the techniques by evaluating their applicability to various aspects of the compatibility problemThe work described in section on substitutability check is based on a 2005 Formal Methods paper, Dynamic Component Substitutability, Lecture Notes in Computer Science 3582, 2005 by the same authors.. [ABSTRACT FROM AUTHOR]

XML transformations are most naturally defined as recursive functions on trees. A naive implementation, however, would load the entire input XML tree into memory before processing. In contrast, programs in stream processing style minimise memory usage since it may release the memory occupied by the processed prefix of the input, but they are harder to write because the programmer is left with the burden to maintain a state. In this paper, we propose a model for XML stream processing and show that all programs written in a particular style of recursive functions on XML trees, the macro forest transducer, can be automatically translated to our stream processors. The stream processor is declarative in style, but can be implemented efficiently by a pushdown machine. We thus get the best of both worlds — program clarity, and efficiency in execution. [ABSTRACT FROM AUTHOR]

Partial Redundancy Elimination (PRE) is a standard program optimization which removes redundant computations via Code Motion. It subsumes and generalizes the optimizations of Global Common Subexpression Elimination (GCSE) and Loop Invariant Code Motion (LICM). Recent work has generalized PRE to become Speculative PRE (SPRE), which uses estimates of execution frequencies to find the optimal places in a program to perform computations. However, the analysis performed by the compiler is computationally intensive and hence impractical for just-in-time (JIT) compilers. This paper introduces a novel approach which abandons a guarantee of optimality in favour of simplicity and speed of analysis. This new approach, called Isothermal SPRE, achieves results which are close to optimal in practice, yet its analysis time is at least as good as current compiler techniques for code motion. It is a technique suitable for use in JIT compilers. [ABSTRACT FROM AUTHOR]

For a long time, one of the major research goals in the computer science research community has been to raise the level of abstraction power of specification languages/programming languages. Many specification languages and formalisms have been invented, but unfortunately very few of those are practically useful, due to limited computer support of these languages and/or inefficient implementations. Thus, one important goal is executable specification languages of high abstraction power and with high performance, good enough for practical usage and comparable in execution speed to hand implementations of applications in low-level languages such as C or C++. In this paper we briefly describe our work in creating efficient executable specification languages for two application domains. The first area is formal specification of programming language semantics, whereas the second is formal specification of complex systems for which we have developed an object-oriented mathematical modeling language called Modelica, including architectural support for components and connectors. Based on these efforts, we are currently working on a unified equation-based mathematical modeling language that can handle modeling of items as diverse as programming languages, computer algebra, event-driven systems, and continuous-time physical systems. The key unifying feature is the notion of equation. In this paper we describe the design and implementation of the unified language. A compiler implementation is already up and running, and used for substantial applications. [ABSTRACT FROM AUTHOR]

Multimedia application development requires features and concepts currently not supported by common systems programming languages. This paper introduces two new minimal language extensions increasing expressive power, safety and optimization possibilities in multimedia programming. New loop statements are presented to shorten multidimensional array access and optimize its execution. Furthermore, a new data type concept is presented to allow quality of service (QoS) definition on data type declaration level. Both have been implemented in Modula-3 and C#. [ABSTRACT FROM AUTHOR]

Type abstraction in object-oriented languages mainly embodies two techniques with different strenghts and weaknesses. The first technique is extension, yielding abstraction mechanisms with good support for gradual specification; the prime example is inheritance. The second technique is functional abstraction, yielding more precise knowledge about the outcome; the prime example is type parameterized classes. This paper argues that they should be clearly separated to work optimally. We have applied this design philosophy to a language based on an extension mechanism, namely virtual classes. As a result, a kind of type parameters have been introduced, but they are simple and only used where they excel. Conversely, final definitions of virtual classes have been removed from the language, thus making virtual classes more flexible. The resulting language presents a clearer and more flexible trade-off between extensibility and predictability, empowering programmers to choose the right balance. [ABSTRACT FROM AUTHOR]

Today's programming platforms do not provide sufficient constructs that allow a program's behavior to depend on the context in which it is executing. This paper presents the design and implementation of programming language extensions that explicitly support our vision of Context-oriented Programming. In this model, programs can be partitioned into layers that can be dynamically activated and deactivated depending on their execution context. Layers are sets of partial program definitions that can be composed in any order. Context-oriented Programming encourages rich, dynamic modifications of program behavior at runtime, requiring an efficient implementation. We present a dynamic representation of layers that yields competitive performance characteristics for both layer activation/deactivation and overall program execution. We illustrate the performance of our implementation by providing an alternative solution for one of the prominent examples of aspect-oriented programming. [ABSTRACT FROM AUTHOR]

This paper describes the application of Real-Time Maude to the formal specification, simulation, and further formal analysis of the sophisticated state-of-the-art OGDC wireless sensor network algorithm. Wireless sensor networks in general, and the OGDC algorithm in particular, pose many challenges to their formal specification and analysis, including novel communication forms, treatment of geographic areas, time-dependent and probabilistic features, and the need to analyze both correctness and performance. Real-Time Maude extends the rewriting logic tool Maude to support formal specification and analysis of object-based real-time systems. This paper explains how we formally specified OGDC in Real-Time Maude, how we could simulate our specification to perform all the analyses done by the algorithm developers using the network simulation tool ns-2, and how we could perform further formal analyses which are beyond the capabilities of simulation tools. A remarkable result is that our Real-Time Maude simulations seem to provide a much more accurate estimate of the performance of OGDC than the ns-2 simulations. To the best of our knowledge, this is the first time a formal tool has been applied to an advanced wireless sensor network algorithm. [ABSTRACT FROM AUTHOR]

In this paper we propose a framework for modeling mobile information systems. Mobility introduces several challenges and issues that impact the development of mobile systems. As a result, we want applications running on mobile devices to exhibit certain traits; they should be aware of the mobility and be adaptive to the changes that occur due to it. Literature has identified several types of mobility - among them, physical and logical mobility. The former pertains to tangible mobile entities like cars, devices and people, while the latter encompasses mobile software entities. In addition to these, this paper includes the concept of vertical mobility - the movement of a network connection between overlapping networks - in a UML profile for modeling mobile information systems. We discuss our experiences from a case study described in [1] , where we modeled a simple mobile information system and transformed parts of the model into code. [ABSTRACT FROM AUTHOR]

Ubiquitous computing environments are characterised by a high number of heterogeneous devices that generate a huge amount of context data. These data are used to adapt applications to changing execution contexts. However, legacy frameworks fail to process context information in a scalable and efficient manner. In this paper, we propose to organise the classical functionalities of a context manager to introduce a 3-steps cycle of data collection, interpretation, and situation identification. We propose the COSMOS framework, which is based on the concepts of context node and context management policies translated into software components in software architecture. This paper presents COSMOS and evaluates its efficiency throughout the example of the composition of context information to implement a caching/off-loading adaptation situation. [ABSTRACT FROM AUTHOR]

Migration of running application code is considered a very attractive and desired mechanism to improve application performance, resource sharing, self-adaptability, etc. This mechanism seems to be even more important nowadays, considering the growing interest in the area of mobile computing and mobile networks. This paper briefly presents a migration mechanism for a CORBA Component Model platform. We discuss general issues related to migration of running code, further elaborated in the context of CCM. We also propose an extension to the original CCM model which provides interfaces to implement migration. The paper presents the most important problems which appeared during implementation of a prototype facility and it discusses possible solutions. One of the most fundamental issues related to mobility of running code is the residual dependency problem. The intention of the work is not to provide a solution to this (possibly unsolvable) problem, but to propose an approach which would make programmers aware of its existence. Thus, the paper allows readers to make more conscious decisions when designing their components. The paper ends with an evaluation of the prototype implementation on top of OpenCCM, an open source Java implementation of the CORBA Component Model. [ABSTRACT FROM AUTHOR]

In this paper we shall survey and discuss in detail the work on the relative expressiveness of recursion and replication in various process calculi. Namely, CCS, the π-calculus, the Ambient calculus, Concurrent Constraint Programming and calculi for Cryptographic Protocols. We shall give evidence that the ability of expressing recursive behaviour via replication often depends on the scoping mechanisms of the given calculus which compensate for the restriction of replication. [ABSTRACT FROM AUTHOR]

Metaprogramming and computational reflection are two related techniques that allow the programmer to change the semantics of a program in a modular fashion. Although the concepts have been explored by researchers for some time, a form of metaprogramming, namely aspect-oriented programming, is now being used by some practitioners. This paper is an attempt to understand the limitations of different forms of computational reflection in concurrent and distributed computing. It specifically studies the use of aspect-oriented programming and reflective actor libraries, and their relation to full reflection. We choose distributed monitoring as the primary example application because its requirements nicely fit the abilities of the two systems as well as illustrate their limitations. [ABSTRACT FROM AUTHOR]

Rebeca is an actor-based language with a formal foundation for modeling concurrent and distributed systems which is designed in an effort to bridge the gap between formal verification approaches and real applications. Rebeca is supported by a tool-set for model checking Rebeca models. Inherent characteristics of Rebeca are used to introduce compositional verification, abstraction, symmetry and partial order reduction techniques for reducing the state space. Simple message-driven object-based computational model, Java-like syntax, and set of verification tools make Rebeca an interesting and easy-to-learn model for practitioners. This paper is to present theories, applications, and supporting tools of Rebeca in a consistent and distilled form. [ABSTRACT FROM AUTHOR]

In this paper, we give an overview on some algorithms for learning automata. Starting with Biermann's and Angluin's algorithms, we describe some of the extensions catering for specialized or richer classes of automata. Furthermore, we survey their recent application to verification problems. [ABSTRACT FROM AUTHOR]

This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the gap between elementary introductions using toy examples and state-of-art case studies by going through a self-contained, yet non-trivial, example. It is hoped that this contributes to explain the problems encountered in verification of imperative, object-oriented programs to a readership outside the limited community of active researchers. [ABSTRACT FROM AUTHOR]

Testing application behavior in the presence of I/O failures is extremely difficult. The resources used for testing usually work without failure. Failures typically cannot be initiated on the test suite level and are usually not tested sufficiently. Essentially, each interaction of the application with the environment can result in a failure. The Enforcer tool identifies such potential failures and automatically tests all relevant outcomes of such actions. It combines the structure of unit tests with coverage information and fault injection. By taking advantage of a unit test infrastructure, performance can be improved by orders of magnitude compared to previous approaches. This paper introduces the usage of the Enforcer tool. [ABSTRACT FROM AUTHOR]

In component-based development, the correctness of a system depends on the correctness of the individual components and on their interactions. Model-based testing is a way of checking the correctness of a component by means of executing test cases that are systematically generated from a model of the component. This model should include the behaviour of how the component can be invoked, as well as how the component itself invokes other components. In many situations, however, only a model that specifies how others can use the component, is available. In this paper we present an approach for model-based testing of components where only these available models are used. Test cases for testing whether a component correctly reacts to invocations are generated from this model, whereas the test cases for testing whether a component correctly invokes other components, are generated from the models of these other components. A formal elaboration is given in the realm of labelled transition systems. This includes an implementation relation, called eco, which formally defines when a component is correct with respect to the components it uses, and a sound and exhaustive test generation algorithm for eco. [ABSTRACT FROM AUTHOR]

Global value numbering (GVN) is an important static analysis technique both for optimizing compilers and program verification tools. Existing complete GVN algorithms discovering all Herbrand equivalences are all inefficient. One reason of this is the intrinsic exponential complexity of the problem, but in practice, since the exponential case is quite rare, the more important reason is the huge data structures annotated to every program point and slow abstract evaluations on them site by site. In this paper, we present an SSA-based algorithm for complete GVN, which uses just one global graph to represent all equivalences at different program points and performs fast abstract evaluations on it. This can be achieved because in SSA form, interferences among equivalence relations at different program points can be entirely resolved with dominance information. We implement the new algorithm in GCC. The average proportion of execution time of the new algorithm in the total compilation time is only 0.36%. To the best of our knowledge, this is the first practical complete GVN algorithm. [ABSTRACT FROM AUTHOR]

This paper shows the equivalence for provability between two infinitary systems with the ω-rule. One system is the positive one-sided fragment of Peano arithmetic without Exchange rules. The other system is two-sided Heyting Arithmetic plus the law of Excluded Middle for $\Sigma^0_1$-formulas, and it includes Exchange. Thus, the logic underlying positive Arithmetic without Exchange, a substructural logic, is shown to be a logic intermediate between Intuitionism and Classical Logic, hence a subclassical logic. As a corollary, the authors derive the equivalence for positive formulas among provability in those two systems and validity in two apparently unrelated semantics: Limit Computable Mathematics, and Game Semantics with 1-backtracking. [ABSTRACT FROM AUTHOR]

A remarkable result in [4] shows that in spite of its being less expressive than CCS w.r.t. weak bisimilarity, CCS! (a CCS variant where infinite behavior is specified by using replication rather than recursion) is Turing powerful. This is done by encoding Random Access Machines (RAM) in CCS!. The encoding is said to be non-faithful because it may move from a state which can lead to termination into a divergent one which do not correspond to any configuration of the encoded RAM. I.e., the encoding is not termination preserving. In this paper we study the existence of faithful encodings into CCS! of models of computability strictly less expressive than Turing Machines. Namely, grammars of Types 1 (Context Sensitive Languages), 2 (Context Free Languages) and 3 (Regular Languages) in the Chomsky Hierarchy. We provide faithful encodings of Type 3 grammars. We show that it is impossible to provide a faithful encoding of Type 2 grammars and that termination-preserving CCS! processes can generate languages which are not Type 2. We finally show that the languages generated by termination-preserving CCS! processes are Type 1 . [ABSTRACT FROM AUTHOR]

Given the combinatorial nature of cellular signalling pathways, where biological agents can bind and modify each other in a large number of ways, concurrent or agent-based languages seem particularly suitable for their representation and simulation [1,2,3,4]. Graphical modelling languages such as κ [5, 6, 7, 8], or the closely related BNG language [9,10,11,12,13,14], seem to afford particular ease of expression. It is unclear however how such models can be implemented. Even a simple model of the EGF receptor signalling network can generate more than $\oldstylenums{10^{23}}$ non-isomorphic species [5], and therefore no approach to simulation based on enumerating species (beforehand, or even on-the-fly) can handle such models without sampling down the number of potential generated species. We present in this paper a radically different method which does not attempt to count species. The proposed algorothm uses a representation of the system together with a super-approximation of its ‘event horizon' (all events that may happen next), and a specific correction scheme to obtain exact timings. Being completely local and not based on any kind of enumeration, this algorithm has a per event time cost which is independent of (i) the size of the set of generable species (which can even be infinite), and (ii) independent of the size of the system (ie, the number of agent instances). We show how to refine this algorithm, using concepts derived from the classical notion of causality, so that in addition to the above one also has that the even cost is depending (iii) only logarithmically on the size of the model (ie, the number of rules). Such complexity properties reflect in our implementation which, on a current computer, generates about $\oldstylenums{10^6}$ events per minute in the case of the simple EGF receptor model mentioned above, using a system with $\oldstylenums{10^5}$ agents. [ABSTRACT FROM AUTHOR]

This paper studies types and probabilistic bisimulations for a timed π-calculus as an effective tool for a compositional analysis of probabilistic distributed behaviour. The types clarify the role of timers as interface between non-terminating and terminating communication for guaranteeing distributed liveness. We add message-loss probabilities to the calculus, and introduce a notion of approximate bisimulation that discards transitions below a certain specified probability threshold. We prove this bisimulation to be a congruence, and use it for deriving quantitative bounds for practical protocols in distributed systems, including timer-driven message-loss recovery and the Two-Phase Commit protocol. [ABSTRACT FROM AUTHOR]

Gordon and Jeffrey developed a type system for checking correspondence assertions. The correspondence assertions, proposed by Woo and Lam, state that when a certain event (called an "end" event) happens, the corresponding "begin" event must have occurred before. They can be used for checking authenticity in communication protocols. In this paper, we refine Gordon and Jeffrey's type system and develop a polynomial-time type inference algorithm, so that correspondence assertions can be verified fully automatically, without any type annotations. The main key idea that enables polynomial-time type inference is to introduce fractional effects; Without the fractional effects, the type inference problem is NP-hard. [ABSTRACT FROM AUTHOR]

This paper presents the programming language Persistent Oberon, which offers persistence as a naturally inbuilt concept. Program data is automatically kept durable and stored in non-volatile memory, without the programmer having to write explicit code for the interactions with an external database system. In the case of a system interruption or failure, the program can directly continue from its latest consistent state. In contrast to other existent persistent programming languages, this language does not need any artificial programming interfaces or commands to use persistence. The programming language is completely implemented and offers a high scalability and performance. [ABSTRACT FROM AUTHOR]

Pattern matching makes ML programs more concise and readable, and these qualities are also sought in object-oriented settings. However, objects and classes come with open class hierarchies, extensibility requirements and the need for data abstraction, which all conflict with matching on concrete data types. Extractor-based pattern matching has been proposed to address this conflict. Extractors are user-defined methods that perform the task of value discrimination and deconstruction during pattern matching. In this paper, we give the first formalization of extractor-based matching, using a first-order object-oriented calculus. We give a direct operational semantics and prove it sound. We then present an optimizing translation to a target language without matching, and prove a correctness result stating that an expression is equivalent to its translation. [ABSTRACT FROM AUTHOR]

State-of-the-art dynamic middleware uses information about the environment in order to evaluate alternative configurations of an application and select one according to some criteria. In the context of applications sensitive to Quality of Service, we have identified the need for a platform independent description of configurations that includes non-functional behaviour, and that allows handling of a large number of application configurations. In this paper, we present a modelling principle and a service plan concept, which together represents such a description. The modelling principle and plan concept extend state-of-the-art with i) a model of the alternative configurations that ensure a minimum of reconfiguration steps; ii) a specification that contains information elements of the configuration, dependencies to the environment, and QoS characteristics; and iii) a platform independent specification. In the paper, we also perform a qualitative assessment of our approach, and we describe a proof-of-concept implementation. [ABSTRACT FROM AUTHOR]

This paper addresses a problem of integrating the consistency management of session guarantees with recovery mechanisms in distributed mobile systems. To solve such a problem, rollback-recovery protocol rVsSG, preserving session guarantees is proposed. The protocol employs known rollback-recovery techniques, however, while applying them, the semantics of session guarantees is taken into account. Consequently, rVsSG protocol is optimized with respect to session guarantees requirements. The paper includes the proof of safety property of the presented protocol. Keywords: fault tolerance, rollback-recovery, mobile systems, session guarantees. [ABSTRACT FROM AUTHOR]

Today many interactions are carried out online through Web sites and e-services and often private and/or sensitive information is required by service providers. A growing concern related to this widespread diffusion of on-line applications that collect personal information is that users' privacy is often poorly managed and sometimes abused. For instance, it is well known how personal information is often disclosed to third parties without the consent of legitimate data owners or that there are professional services specialized on gathering and correlating data from heterogeneous repositories, which permit to build user profiles and possibly to disclose sensitive information not voluntarily released by their owners. For these reasons, it has gained great importance to design systems able to fully preserve information privacy by managing in a trustworthy and responsible way all identity and profile information. In this paper, we investigate some problems concerning identity management for e-services and present the architecture of the Access Control Decision Function, a software component in charge of managing access request in a privacy-aware fashion. The content of this paper is a result of our ongoing activity in the framework of the PRIME project (Privacy and Identity Management for Europe) [18], funded by the European Commission, whose objective is the development of privacy-aware solutions for enforcing security. [ABSTRACT FROM AUTHOR]

Emerging component-based software development architectures promise better re-use of software components, greater flexibility, scalability and higher quality of services. But like any other piece of software too, software components are hardly perfect, when being created. Problems and bugs have to be fixed and new features need to be added. This paper will give an introduction to the problem of component evolution and the syntactical incompatibilities which result during necessary multi component upgrades. The authors present an approach for the detection of such incompatibilities between multiple generations of component revisions basing on a formal interface model. The main concern of the paper will be the automated reconfiguration of component based software systems by intelligent swapping of component revisions to find conflict free system states. [ABSTRACT FROM AUTHOR]

Component adaptation needs to be taken into account when developing trustworthy systems, where the properties of component assemblies have to be reliably obtained from the properties of its constituent components. Thus, a more systematic approach to component adaptation is required when building trustworthy systems. In this paper, we illustrate how (design and architectural) patterns can be used to achieve component adaptation and thus serve as the basis for such an approach. The paper proposes an adaptation model which is built upon a classification of component mismatches, and identifies a number of patterns to be used for eliminating them. We conclude by outlining an engineering approach to component adaptation that relies on the use of patterns and provides additional support for the development of trustworthy component-based systems. [ABSTRACT FROM AUTHOR]

Frameworks are large building blocks of systems, encapsulating the commonalities of a family of applications. For reuse of these common features, frameworks are instantiated by smaller-sized components, plugins, to specific products. However, the framework instantiation process is often difficult, because not all aspects of the interplay of the framework and its plugins can be captured by standard type systems. Application developers instantiating a framework often fail to develop correct applications. Thus, this paper surveys several typical framework instantiation problems. A simple facet-based classification of the problems is given. It is shown how the different problem classes are related to phases of the software process and how they can be tackled appropriately. Finally, the paper derives several research challenges, in particular, the challenge to define appropriate framework instantiation languages. [ABSTRACT FROM AUTHOR]

We consider in this paper that a DSL (Domain Specific Language) may be defined by a set of models. A typical DSL is the ATLAS Transformation Language (ATL). An ATL program transforms a source model (conforming to a source metamodel) into a target model (conforming to a target metamodel). Being itself a model, the transformation program conforms to the ATL metamodel. The notion of metamodel is thus used to define the source DSL, the target DSL and the transformation DSL itself. As a consequence we can see that agility to define metamodels and precision of these definitions is of paramount importance in any model engineering activity. In order to fullfill the goals of agility and precision in the definition of our metamodels, we have been using a notation called KM3 (Kernel MetaMetaModel). KM3 may itself be considered as a DSL for describing metamodels. This paper presents the rationale for using KM3, some examples of its use and a precise definition of the language. [ABSTRACT FROM AUTHOR]

In the past, several model checking algorithms have been proposed to verify probabilistic reactive systems. In contrast to the non-probabilistic setting where various techniques have been suggested and successfully applied to combat the state space-explosion problem in the context of model checking the techniques used for probabilistic systems have mainly concentrated on symbolic methods with variants of decision diagrams or abstraction methods. Only recently results have been published that give criteria on applying partial order reduction for verifying quantitative linear time properties as well as branching time properties for probabilistic systems. This paper summarizes the results that have been established so far about partial order reduction for Markov decision processes. We present the different reduction conditions and provide a comparison of the corresponding results. [ABSTRACT FROM AUTHOR]

A program verifier is a complex system that uses compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user interface. This paper describes the architecture of a state-of-the-art program verifier for object-oriented programs. [ABSTRACT FROM AUTHOR]

A well-defined boundary of components allows to encapsulate internal state and to distinguish between internal calls that remain inside the component and external calls that have target objects outside the component. From a static point of view, such boundaries define the programmer's interface to the component. In particular, they define the methods that can be called on the component. From a dynamic point of view, the boundaries separate the component state and those parts of the program state outside the component. In this tutorial paper, we investigate encapsulated components that are realized based on object-oriented concepts. We define a semantics that captures a flexible notion of hierarchical encapsulation with confined references. The semantics generalizes the encapsulation concepts of ownership types. It is used as a foundation for modular behavioral component specifications. In particular, it allows to provide a simple semantics for invariants and an alternative solution for the frame problem. We demonstrate this new specification methodology by typical programming patterns. [ABSTRACT FROM AUTHOR]

The incorrect use of pointers is one of the most common source of software errors. Concurrency has a similar characteristic. Proving the correctness of concurrent pointer manipulating programs, let alone algorithmically, is a highly non-trivial task. This paper proposes an automated verification technique for concurrent programs that manipulate linked lists. Key issues of our approach are: automata (with fairness constraints), heap abstractions that are tailored to the program and property to be checked, first-order temporal logic, and a tableau-based model-checking algorithm. [ABSTRACT FROM AUTHOR]

In this paper we survey abstraction and refinement in model checking. We restrict the discussion to existential abstraction which over-approximates the behaviors of the concrete model. The logics preserved under this abstraction are the universal fragments of branching-time temporal logics as well as linear-time temporal logics. For simplicity of presentation, we also restrict the discussion to abstraction functions, rather then abstraction relations. Thus, every concrete state is represented by exactly one abstract state. An abstract state then represents a set of concrete states, which is disjoint from the sets represented by other abstract states. [ABSTRACT FROM AUTHOR]

STAIRS is a method for the compositional development of interactions in the setting of UML 2.0. In addition to defining denotational trace semantics for the main aspects of interactions, STAIRS focuses on how interactions may be developed through successive refinement steps. In this tutorial paper, we concentrate on explaining the practical relevance of STAIRS. Guidelines are given on how to create interactions using the different STAIRS operators, and how these may be refined. The pragmatics is illustrated by a running example. [ABSTRACT FROM AUTHOR]

Separation logic is a program logic for reasoning about programs that manipulate pointer data structures. We describe Smallfoot, a tool for checking certain lightweight separation logic specifications. The assertions describe the shapes of data structures rather than their detailed contents, and this allows reasoning to be fully automatic. The presentation in the paper is tutorial in style. We illustrate what the tool can do via examples which are oriented toward novel aspects of separation logic, namely: avoidance of frame axioms (which say what a procedure does not change); embracement of "dirty" features such as memory disposal and address arithmetic; information hiding in the presence of pointers; and modular reasoning about concurrent programs. [ABSTRACT FROM AUTHOR]

This tutorial paper describes a framework for modelling several aspects of distributed computing based on Synchronised Hyperedge Replacement (SHR), a graph rewriting formalism. Components are represented as edges and they rewrite themselves by synchronising with neighbour components the productions that specify their behaviour. The SHR framework has been equipped with many formal devices for representing complex synchronisation mechanisms which can tackle mobility, heterogeneous synchronisations and non-functional aspects, key factors of Service Oriented Computing (SOC). We revise the SHR family as a suitable model for contributing to the formalisation of SOC systems. [ABSTRACT FROM AUTHOR]