nach oben

2005 | Buch

Kapitel lesen Erstes Kapitel lesen

Fundamental Approaches to Software Engineering

8th International Conference, FASE 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings

herausgegeben von: Maura Cerioli

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

ETAPS 2005 was the eighth instance of the European Joint Conferences on Theory and Practice of Software. ETAPS is an annual federated conference that was established in 1998 by combining a number of existing and new conf- ences. This year it comprised ?ve conferences (CC, ESOP, FASE, FOSSACS, TACAS), 17 satellite workshops (AVIS, BYTECODE, CEES, CLASE, CMSB, COCV, FAC, FESCA, FINCO, GCW-DSE, GLPL, LDTA, QAPL, SC, SLAP, TGC, UITP), seven invited lectures (not including those that were speci?c to the satellite events), and several tutorials. We received over 550 submissions to the ?ve conferences this year, giving acceptance rates below 30% for each one. Congratulations to all the authors who made it to the ?nal program! I hope that most of the other authors still found a way of participating in this exciting event and I hope you will continue submitting. The events that comprise ETAPS address various aspects of the system - velopment process, including speci?cation, design, implementation, analysis and improvement. The languages, methodologies and tools which support these - tivities are all well within its scope. Di?erent blends of theory and practice are represented, with an inclination towards theory with a practical motivation on the one hand and soundly based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware s- tems,andtheemphasisonsoftwareisnotintendedtobeexclusive.

Inhaltsverzeichnis

Frontmatter

Invited Contributions

Esterel v7: From Verified Formal Specification to Efficient Industrial Designs

Abstract

Synchronous languages were developed in the mid-80’s specifically to deal with embedded systems. They are based on mathematical semantics and support formal compilation to classical software or hardware languages as well as formal verification. Esterel v7 is a major industrial evolution of the original Esterel synchronous language, mostly directed to complex hardware applications. The language is supported by the Esterel Studio integrated development environment, which provides a smooth path from verifiable executable specification to efficient circuit synthesis. The graphical Safe States Machines derived from Esterel are also used in the SCADE tool which is widely used for safety-critical software applications in avionics.

Gérard Berry

Checking Memory Safety with Blast

Abstract

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how Blast can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use Ccured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that Blast can remove many of the run-time checks added by Ccured and provide useful information to the programmer about many of the remaining checks.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Web Services

Analyzing Web Service Based Business Processes

Abstract

This paper is concerned with the application of Web services to distributed, cross-organizational business processes. In this scenario, it is crucial to answer the following questions: Do two Web services fit together in a way such that the composed system is deadlock-free? – the question of compatibility. Can one Web service be replaced by another while the remaining components stay untouched? – the question of equivalence. Can we reason about the soundness of one given Web service without considering the actual environment it will by used in?

This paper defines the notion of usability – an intuitive and locally provable soundness criterion for a given Web services. Based on this notion, this paper demonstrates how the other questions could be answered. The presented method is based on Petri nets, because this formalism is widely used for modeling and analyzing business processes. Due to the existing Petri net semantics for BPEL4WS – a language that is in the very act of becoming the industrial standard for Web service based business processes – the results are directly applicable to real world examples.

Axel Martens

Automatic Conformance Testing of Web Services

Abstract

Web Services are the basic building blocks of next generation Internet applications, based on dynamic service discovery and composition. Dedicated discovery services will store both syntactic and behavioral descriptions of available services and guarantee their compatibility with the requirements expressed by clients. In practice, however, interactions may still fail because the Web Service’s implementation may be faulty. In fact, the client has no guarantee on the quality of the implementation associated to any service description.

In this paper, we propose the idea of high-quality service discovery incorporating automatic testing for validating Web Services before allowing their registration. First, the discovery service automatically generates conformance test cases from the provided service description, then runs the test cases on the target Web Service, and only if the test is successfully passed, the service is registered.

In this way, clients bind with Web Services providing a compatible signature, a suitable behavior, and a high-quality implementation.

Reiko Heckel, Leonardo Mariani

Graph Grammars and Graph Transformations

Termination Criteria for Model Transformation

Abstract

Model Transformation has become central to most software engineering activities. It refers to the process of modifying a (usually graphical) model for the purpose of analysis (by its transformation to some other domain), optimization, evolution, migration or even code generation. In this work, we show termination criteria for model transformation based on graph transformation. This framework offers visual and formal techniques based on rules, in such a way that model transformations can be subject to analysis. Previous results on graph transformation are extended by proving the termination of a transformation if the rules applied meet certain criteria. We show the suitability of the approach by an example in which we translate a simplified version of Statecharts into Petri nets for functional correctness analysis.

Hartmut Ehrig, Karsten Ehrig, Juan de Lara, Gabriele Taentzer, Dániel Varró, Szilvia Varró-Gyapay

Ensuring Structural Constraints in Graph-Based Models with Type Inheritance

Abstract

Graphs are a common means to represent structures in models and meta-models of software systems. In this context, the description of model domains by classifying the domain entities and their relations using class diagrams or type graphs has emerged as a very valuable principle. The constraints that can be imposed by pure typing are, however, relatively weak; it is therefore common practice to enrich type information with structural properties (such as local invariants or multiplicity conditions) or inheritance.

In this paper, we show how to formulate structural properties using graph constraints in type graphs with inheritance, and we show how to translate constrained type graphs with inheritance to equivalent constrained simple type graphs. From existing theory it then follows that graph constraints can be translated into pre-conditions for productions of a typed graph transformation system which ensures those graph constraints. This result can be regarded as a further important step of integrating graph transformation with object-orientation concepts.

Gabriele Taentzer, Arend Rensink

Modelling Parametric Contracts and the State Space of Composite Components by Graph Grammars

Abstract

Modeling the dependencies between provided and required services within a software component is necessary for several reasons, such as automated component adaptation and architectural dependency analysis. Parametric contracts for software components specify such dependencies and were successfully used for automated protocol adaptation and quality of service prediction. In this paper, a novel model for parametric contracts based on graph grammars is presented and a first definition of the compositionality of parametric contracts is given. Compared to the previously used finite state machine based formalism, the graph grammar formalism allows a more elegant formulation of parametric contract applications and considerably simpler implementations.

Ralf H. Reussner, Jens Happe, Annegret Habel

Components

Improving the Build Architecture of Legacy C/C++ Software Systems

Abstract

The build architecture of legacy C/C++ software systems, groups program files in directories to represent logical components. The interfaces of these components are loosely defined by a set of header files that are typically grouped in one common include directory. As legacy systems evolve, these interfaces decay, which contribute to an increase in the build time and the number of conflict in parallel developments. This paper presents an empirical study of the build architecture of large commercial software systems, introduces a restructuring approach, based on Reflexion models and automatic clustering, and reports on a case study using VIM open source editor.

Homayoun Dayani-Fard, Yijun Yu, John Mylopoulos, Periklis Andritsos

Using Scenarios to Predict the Reliability of Concurrent Component-Based Software Systems

Abstract

Scenarios are a popular means for capturing behavioural requirements of software systems early in the lifecycle. Scenarios show how components interact to provide system level functionality. If component reliability information is available, scenarios can be used to perform early system reliability assessment. In this paper we present a novel automated approach for predicting software system reliability. The approach involves extending a scenario specification to model (1) the probability of component failure, and (2) scenario transition probabilities derived from an operational profile of the system. From the extended scenario specification, probabilistic behaviour models are synthesized for each component and are then composed in parallel into a model for the system. Finally, a user-oriented reliability model described by Cheung is used to compute a reliability prediction from the system behaviour model. The contribution of this paper is a reliability prediction technique that takes into account the component structure exhibited in the scenarios and the concurrent nature of component-based systems. We also show how implied scenarios induced by the component structure and system behaviour described in the scenarios can be used to evolve the reliability prediction.

Genaína Rodrigues, David Rosenblum, Sebastian Uchitel

Augmenting UML Models for Composition Conflict Analysis

Abstract

Component reuse is inhibited by two factors: Lack of an adequate modeling representation of components and lack of a method to predict properties of a composition of application components. In this paper, we propose a framework for conflict identification. The framework is primarily based on a taxonomy describing communication and technology related properties. Conflict identification is based on inference rules. Furthermore, we aim to integrate conflict reasoning in the software development process. We will show that the Unified Modeling Language and the Resource Description Framework can be combined to provide a solution to the representation problems, without resorting to extension mechanisms, and without limiting to a specific component platform. As a real life example, we model the connection of an .Net Serviced Component to an Enterprise Java Bean as part of a mortgage bank’s enterprise architecture and prove its viability.

Andreas Leicher, Jörn Guy Süß

A Tool to Automate Component Clustering and Identification

Abstract

It is a key activity in CBD to identify high-quality components which have high cohesion and low coupling. However, component clustering is carried out in manual fashion by developers, resulting excessive time consumption and generating errors. In this article, we present an implementation of a tool which automates a component clustering and identification method. We show how we realize a clustering method as a tool and explain techniques applied in the implementation. Using the tool, component identification can be automated, and one can generate and navigate multiple configurations to find the most appropriate one for the project effortlessly.

Soo Ho Chang, Man Jib Han, Soo Dong Kim

Product Lines

Managing Variability Using Heterogeneous Feature Variation Patterns

Abstract

Feature-driven variability is viewed as an instance of multi-dimensional separation of concerns. We argue that feature variation concerns can be presented as pattern-like entities – called feature variation patterns – cross-cutting heterogeneous artifacts. We show that a feature variation pattern, covering a wide range of artifact types from a feature model to implementation, can be used to manage feature-driven variability in a software development process. A prototype tool environment has been developed to demonstrate the idea, supporting the specification and use of heterogeneous feature variation patterns. We illustrate the idea with a small example taken from J2EE, and further study the practical applicability of the approach in an industrial product-line.

Imed Hammouda, Juha Hautamäki, Mika Pussinen, Kai Koskimies

Color-Blind Specifications for Transformations of Reactive Synchronous Programs

Abstract

Execution environments are used as specifications for specialization of input-output programs in the derivation of product lines. These environments, formalized as color-blind I/O-alternating transition systems, are tolerant to mutations in a given program’s outputs. Execution environments enable new compiler optimizations, vastly exceeding usual reductions. We propose a notion of context-dependent refinement for I/O-alternating transition systems, which supports composition and hierarchical reuse. The framework is demonstrated by discussing adaptations to realistic design languages and by presenting an exampleof a product line.

Kim G. Larsen, Ulrik Larsen, Andrzej Wasowski

Theory

On the Correspondence Between Conformance Testing and Regular Inference

Abstract

Conformance testing for finite state machines and regular inference both aim at identifying the model structure underlying a black box system on the basis of a limited set of observations. Whereas the former technique checks for equivalence with a given conjecture model, the latter techniques addresses the corresponding synthesis problem by means of techniques adopted from automata learning. In this paper we establish a common framework to investigate the similarities of these techniques by showing how results in one area can be transferred to results in the other and to explain the reasons for their differences.

Therese Berg, Olga Grinchtein, Bengt Jonsson, Martin Leucker, Harald Raffelt, Bernhard Steffen

Observational Purity and Encapsulation

Abstract

Practical specification languages for imperative and object-oriented programs, such as JML, Eiffel, and Spec#, allow the use of program expressions including method calls in specification formulas. For coherent semantics of specifications, and to avoid anomalies with runtime assertion checking, expressions in specifications and assertions are typically required to be strongly pure in the sense that their evaluation has no effect on the state of preexisting objects. For specification of large systems using standard libraries this restriction is impractical: it disallows many standard methods that mutate state for purposes such as caching or lazy initialization. Calls of such methods can sensibly be used for specifications and annotations in contexts where their effects cannot be observed. This paper formalizes and extends a recently proposed notion of observational purity, reducing the proof obligation to a familiar one for equivalence of two class implementations.

David A. Naumann

Towards a Theory on the Role of Ontologies in Software Engineering Problem Solving

Abstract

We present and validate a theoretical model of methodological works in Software Engineering that, without claiming for completeness, allows us to investigate the role of ontologies in the problem solving process related with the development of software. Our main conclusion is the potential of ontologies as resources for an individual to think during problem solving. We argument that suitable ontologies can support solving strategies as well as motivate their invention. We also conclude the importance of accompany an ontology with knowledge that guides the engineer in reasoning with its concepts.

The model regards a methodological work as an heterogeneous theory about a class of problems and about a number of conceptual elements. Some of the elements are ontologies, which play the role of identifying and relating aspects of the knowledge about the class of problems, making up novel perspectives on the problems that may promote solving strategies.

For illustration purposes, we take Jackson’s “Problem Frames” as a case study. We analyse this work through the former model, identifying the ontologies, guides, and promoted strategies. Then we propose an alternative ontology, based on that used in the KAOS approach; we reformulate some parts of Jackson’s work through this ontology and propose a strategy as well as some guides.

José M. Cañete, Francisco J. Galán

Code Understanding and Validation

A Framework for Counterexample Generation and Exploration

Abstract

Model-checking is becoming an accepted technique for debugging hardware and software systems. Debugging is based on the “Check / Analyze / Fix” loop: check the system against a desired property, producing a counterexample when the property fails to hold; analyze the generated counterexample to locate the source of the error; fix the flawed artifact – the property or the model. The success of model-checking non-trivial systems critically depends on making this Check / Analyze / Fix loop as tight as possible. In this paper, we concentrate on the Analyze part of the debugging loop. To this end, we present a framework for generating, structuring and exploring counterexamples either interactively or with the help of user-specified strategies.

Marsha Chechik, Arie Gurfinkel

Using Annotations to Check Structural Properties of Classes

Abstract

The specification of meta-information, by using attributes in .NET or annotations in Java, along with the source code is gaining widespread use. Meta-information is used for different purposes such as code generation or configuration of the environment in which a class is deployed. However, in most cases using an annotation also implies that constraints, beyond those defined by the language’s semantics, have to be followed. E.g., a class must define a no-arguments constructor or the parameters of a method must have specific types. Currently, these constraints are not checked at all or only to a very limited extend. Hence, a violation can remain undetected and result in deployment-time or even subtle run-time errors. In this paper, we present a user-extensible framework that enables the definition of constraints to check the properties of annotated elements. Further, we demonstrate the application of the framework to check the constraints defined in the EJB 3.0 specification, and an evaluation of the approach based on checking the xPetstore-EJB3.0 project from within Eclipse to test the performance.

Michael Eichberg, Thorsten Schäfer, Mira Mezini

Improving System Understanding via Interactive, Tailorable, Source Code Analysis

Abstract

In situations in which developers are not familiar with a system or its documentation is inadequate, the system’s source code becomes the only reliable source of information. Unfortunately, source code has much more detail than is needed to understand the system, and it disperses or obscures high-level constructs that would ease the system’s understanding. Automated tools can aid system understanding by identifying recurring program features, classifying the system modules based on their purpose and usage patterns, and analyzing dependencies across the modules. This paper presents an iterative, user-guided approach to program understanding based on a framework for analyzing and visualizing software systems. The framework is built around a pluggable and extensible set of clues about a given problem domain, execution environment, and/or programming language. We evaluate our approach by providing the analysis of our tool’s results obtained from several case studies.

Vladimir Jakobac, Alexander Egyed, Nenad Medvidovic

Kaveri: Delivering the Indus Java Program Slicer to Eclipse

Abstract

This tool paper describes a modular program slicer for Java built using the Indus program analysis framework along with it’s Eclipse-based user interface called Kaveri. Indus provides a library of classes that enables users to quickly assemble a highly customized non-system dependence graph based inter-procedural program slicer capable of slicing concurrent Java programs. Kaveri is an Eclipse plugin that relies on the above library to deliver program slicing to the eclipse platform. Apart from the basic feature for generating program slices from within eclipse along with an intuitive UI to view the slice, the plugin also provides the capability for chasing various dependences in the application to understand the slice.

Ganeshan Jayaraman, Venkatesh Prasad Ranganath, John Hatcliff

The UML

Non-local Choice and Beyond: Intricacies of MSC Choice Nodes

Abstract

MSC is a visual formalism for specifying the behavior of systems. To obtain implementations for individual processes, the MSC choice construction poses fundamental problems. The best-studied cause is non-local choice, which e.g. is unavoidable in systems with autonomous processes. In this paper we characterize two additional problematic classes of choice nodes. Based on these three classes we point out some errors in related work. Extending our work on pragmatic implementations of non-local choice, we motivate a different choice semantics which allows a little more behavior. Finally, inspired by practical case studies, we present the first implementation approach for non-local choice nodes that can handle arbitrary numbers of processes.

Arjan J. Mooij, Nicolae Goga, Judi M. T. Romijn

Coverage Criteria for Testing of Object Interactions in Sequence Diagrams

Abstract

This work defines several control-flow coverage criteria for testing the interactions among a set of collaborating objects. The criteria are based on UML sequence diagrams that are reverse-engineered from the code under test. The sequences of messages in the diagrams are used to define the coverage goals for the family of criteria, in a manner that generalizes traditional testing techniques such as branch coverage and path coverage. We also describe a run-time analysis that gathers coverage measurements for each criterion. To compare the criteria, we propose an approach that estimates the testing effort required to satisfy each criterion, using analysis of the complexity of the underlying sequence diagrams. The criteria were investigated experimentally on a set of realistic Java components. The results of this study compare different approaches for testing of object interactions and provide insights for testers and for builders of test coverage tools.

Atanas Rountev, Scott Kagan, Jason Sawin

Tools for Secure Systems Development with UML: Security Analysis with ATPs

Abstract

We present tool-support for checking the security requirements associated with UMLsec stereotypes. A framework supports implementing verification routines, based on XMI output of the diagrams from UML CASE tools. Advanced users of the UMLsec approach can use this open-source framework to implement verification routines for the constraints of self-defined stereotypes. We focus on a verification routine that automatically verifies sequence diagrams with cryptographic algorithms for security requirements by using automated theorem provers.

Jan Jürjens, Pasha Shabalin

Maintaining Life Perspectives During the Refinement of UML Class Structures

Abstract

Models provide an alternative perspective for the understanding of a software system. However, models reflect the state of the system at the time of their creation (or last updating) but they do not reflect intermediate changes during the system’s evolution. Depicting perspectives without showing changes is like watching a movie through a small set of still pictures (i.e., no motion). This paper demonstrates this problem on an existing technique for the automated simplification (abstraction) of class diagrams. We will show that it is computationally feasible to maintain a set of abstract perspectives of a class structure such that evolutionary changes to the class structure are instantly perceived through its perspectives. For developers, this provides the ability to understand changes to systems from the modeling perspectives they care about. It also gives the developers the confidence that their modeling perspectives remain up-to-date with the system even while the system evolves.

Alexander Egyed, Wuwei Shen, Kun Wang

Automatic Proofs and Provers

Automated Compositional Proofs for Real-Time Systems

Abstract

We present a framework for formally proving that the composition of the behaviors of the different parts of a complex, real-time system ensures a desired global specification of the overall system. The framework is based on a simple compositional rely/guarantee circular inference rule, plus a small set of conditions concerning the integration of the different parts into a whole system. The reference specification language is the TRIO metric linear temporal logic.

The novelty of our approach with respect to existing compositional frameworks — most of which do not deal explicitly with real-time requirements — consists mainly in its generality and abstraction from any assumptions about the underlying computational model and from any semantic characterizations of the temporal logic language used in the specification. Moreover, the framework deals equally well with continuous and discrete time. It is supported by a tool, implemented on top of the proof-checker PVS, to perform deduction-based verification through theorem-proving of modular real-time axiom systems.

As an example of application, we show the verification of a real-time version of the old-fashioned but still relevant “benchmark” of the dining philosophers problem.

Carlo A. Furia, Matteo Rossi, Dino Mandrioli, Angelo Morzenti

Iterative Circular Coinduction for CoCasl in Isabelle/HOL

Abstract

Coalgebra has in recent years been recognized as the framework of choice for the treatment of reactive systems at an appropriate level of generality. Proofs about the reactive behavior of a coalgebraic system typically rely on the method of coinduction. In comparison to ‘traditional’ coinduction, which has the disadvantage of requiring the invention of a bisimulation relation, the method of circular coinduction allows a higher degree of automation. As part of an effort to provide proof support for the algebraic-coalgebraic specification language CoCasl, we develop a new coinductive proof strategy which iteratively constructs a bisimulation relation, thus arriving at a new variant of circular coinduction. Based on this result, we design and implement tactics for the theorem prover Isabelle which allow for both automatic and semiautomatic coinductive proofs. The flexibility of this approach is demonstrated by means of examples of (semi-)automatic proofs of consequences of CoCasl specifications, automatically translated into Isabelle theories by means of the Bremen heterogeneous Casl tool set Hets.

Daniel Hausmann, Till Mossakowski, Lutz Schröder

Formalisation and Verification of Java Card Security Properties in Dynamic Logic

Abstract

We present how common Java Card security properties can be formalised in Dynamic Logic and verified, mostly automatically, with the KeY system. The properties we consider, are a large subset of properties that are of importance to the smart card industry. We discuss the properties one by one, illustrate them with examples of real-life, industrial size, Java Card applications, and show how the properties are verified with the KeY Prover – an interactive theorem prover for Java Card source code based on a version of Dynamic Logic that models the full Java Card standard. We report on the experience related to formal verification of Java Card programs we gained during the course of this work. Thereafter, we present the current state of the art of formal verification techniques offered by the KeY system and give an assessment of interactive theorem proving as an alternative to static analysis.

Wojciech Mostowski

Backmatter

Titel: Fundamental Approaches to Software Engineering
herausgegeben von: Maura Cerioli
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-540-31984-9
Print ISBN: 978-3-540-25420-1
DOI: https://doi.org/10.1007/b107062