Today's technologies are becoming more and more pervasive and advanced software systems can replace human beings in many different tasks. This is especially true in the case of automated decision-making systems based on machine learning (ML). Important ethical implications arise when such decision systems are used in sensitive contexts (e.g., justice or loans). The elicitation of these implications, that is, of the ethical requirements behind ML-based systems is a new challenge we must address to avoid societal risks. This is particularly urgent for fairness since this notion lacks a precise and commonly accepted definition, thus hampering its assessment. This paper aims to give a comprehensive definition of fairness, present a unified taxonomy of alternative interpretations, define a new decision tree that can guide the choice of the correct interpretation, and carry out a preliminary assessment with experiments in a real-world context.

Engineering cyber-physical systems inhabiting contemporary urban spatial environments demands software engineering facilities to support design and operation. Tools and approaches in civil engineering and architectural informatics produce artifacts that are geometrical or geographical representations describing physical spaces. The models we consider conform to the CityGML standard; although relying on international standards and accessible in machine-readable formats, such physical space descriptions often lack semantic information that can be used to support analyses. In our context, analysis as commonly understood in software engineering refers to reasoning on properties of an abstracted model-in this case a city design. We support model-based development, firstly by providing a way to derive analyzable models from CityGML descriptions, and secondly, we ensure that changes performed are propagated correctly. Essentially, a digital twin of a city is kept synchronized, in both directions, with the information from the actual city. Specifically, our formal programming technique and accompanying technical framework assure that relevant information added, or changes applied to the domain (resp. analyzable) model are reflected back in the analyzable (resp. domain) model automatically and coherently. The technique developed is rooted in the theory of bidirectional transformations, which guarantees that synchronization between models is consistent and well behaved. Produced models can bootstrap graph-theoretic, spatial or dynamic analyses. We demonstrate that bidirectional transformations can be achieved in practice on real city models.

Mobile and general-purpose robots increasingly support everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing complex behaviors known as missions. Recognizing this need, a large number of domain-specific specification languages has been proposed. These, in addition to traditional logical languages, allow the use of formally specified missions for synthesis, verification, simulation or guiding implementation. For instance, the logical language LTL is commonly used by experts to specify missions as an input for planners, which synthesize a robot's required behavior. Unfortunately, domain-specific languages are usually tied to specific robot models, while logical languages such as LTL are difficult to use by non-experts. We present a catalog of 22 mission specification patterns for mobile robots, together with tooling for instantiating, composing, and compiling the patterns to create mission specifications. The patterns provide solutions for recurrent specification problems; each pattern details the usage intent, known uses, relationships to other patterns, and—most importantly—a template mission specification in temporal logic. Our tooling produces specifications expressed in the temporal logics LTL and CTL to be used by planners, simulators or model checkers. The patterns originate from 245 mission requirements extracted from the robotics literature, and they are evaluated upon a total of 441 real-world mission requirements and 1251 mission specifications. Five of these reflect scenarios defined with two well-known industrial partners developing human-size robots. We further validate our patterns’ correctness with simulators and two different types of real robots.

Systematic model-driven design and early validation enable engineers to verify that a reactive system does not violate its requirements before actually implementing it. Requirements may come from multiple stakeholders, who are often concerned with different facets - design typically involves different experts having different concerns and views of the system. Engineers start from a specification which may be sourced from some domain model, while validation is often done on state-transition structures that support model checking. Two computationally expensive steps may work against scalability: transformation from specification to state-transition structures, and model checking. We propose a technique that makes the former efficient and also makes the resulting transition systems small enough to be efficiently verified. The technique automatically projects the specification into submodels depending on a property sought to be evaluated, which captures some stakeholder's viewpoint. The resulting reactive system submodel is then transformed into a state-transition structure and verified. The technique achieves cone-of-influence reduction, by slicing at the specification model level. Submodels are analysis-equivalent to the corresponding full model. If stakeholders propose a change to a submodel based on their own view, changes are automatically propagated to the specification model and other views affected. Automated reflection is achieved thanks to bidirectional model transformations, ensuring correctness. We cast our proposal in the context of graph-based reactive systems whose dynamics is described by rewriting rules. We demonstrate our view-based framework in practice on a case study within cyber-physical systems.

Internet-enabled devices operating in the physical world are increasingly integrated in modern distributed systems. We focus on systems where the dynamics of spatial distribution is crucial; in such cases, devices may need to carry out complex computations (e.g., analyses) to check satisfaction of spatial requirements. The requirements are partly global—as the overall system should achieve certain goals—and partly individual, as each entity may have different goals. Assurance may be achieved by keeping a model of the system at runtime, monitoring events that lead to changes in the spatial environment, and performing requirements analysis. However, computationally intensive runtime spatial analysis cannot be supported by resource-constrained devices and may be offloaded to the cloud. In such a scenario, multiple challenges arise regarding resource allocation, cost, performance, among other dimensions. In particular, when the workload is unknown at the system’s design time, it may be difficult to guarantee application-service-level agreements, e.g., on response times. To address and reason on these challenges, we first instantiate complex computations as microservices and integrate them to an IoT-cloud architecture. Then, we propose alternative cloud deployments for such an architecture—based on virtual machines, containers, and the recent Functions-as-a-Service paradigm. Finally, we assess the feasibility and tradeoffs of the different deployments in terms of scalability, performance, cost, resource utilization, and more. We adopt a workload scenario from a known dataset of taxis roaming in Beijing, and we derive other workloads to represent unexpected request peaks and troughs. The approach may be replicated in the design process of similar classes of spatially distributed IoT systems.

Technological advances enable new kinds of smart environments exhibiting complex behaviors; smart cities are a notable example. Smart functionalities heavily depend on space and need to be aware of entities typically found in the spatial domain, e.g. roads, intersections or buildings in a smart city. We advocate a model-based development, where the model of physical space, coming from the architecture and civil engineering disciplines, is transformed into an analyzable model upon which smart functionalities can be embedded. Such models can then be formally analyzed to assess a composite system design. We focus on how a model of physical space specified in the CityGML standard language can be transformed into a model amenable to analysis and how the two models can be automatically kept in sync after possible changes. This approach is essential to guarantee safe model-driven development of composite systems inhabiting physical spaces. We showcase transformations of real CityGML models in the context of scenarios concerning both design time and runtime analysis of space-dependent systems.

Comprehensive privacy mechanisms are essential in the pervasive internet-of-things systems of today, which are comprised of multiple distributed devices and diverse software stacks, while located in different legal or administrative domains. In such systems, often consisting of resource-constrained devices, guarantees of correctness and conformance to privacy policies is required, while data need to be synchronized among different software components. Motivated by the "data protection by design and by default" principle, we propose a technical framework to support data synchronization among edge components tailored for pervasive IoT applications. Our privacy-driven synchronization approach is based on a generically applicable privacy model and able to capture roles and permissions, actions on data, conditions and obligations that arise in privacy requirements. For automated and correct reflection of synchronized data among components, we adopt bidirectional transformations, a mechanism where synchronization between models, consistency, and well-behavedness are formally guaranteed. Thus, automatically generated privacy-aware data transformations are correct by construction. We evaluate POET, our framework and accompanying tool with a case study on medical information privacy and demonstrate its performance in resource-constrained edge devices.

Abstract Controllers often are large and complex reactive software systems and thus they typically cannot be developed as monolithic products. Instead, they are usually comprised of multiple components that interact to provide the desired functionality. Components themselves can be complex and in turn be decomposed into multiple sub-components. Designing such systems is complicated and must follow systematic approaches, based on recursive decomposition strategies that yield a modular structure. This paper proposes FIDDle–a comprehensive verification-driven framework which provides support for designers during development. FIDDle supports hierarchical decomposition of components into sub-components through formal specification in terms of pre- and post-conditions as well as independent development, reuse and verification of sub-components. The framework allows the development of an initial, partially specified design of the controller, in which certain components, yet to be defined, are precisely identified. These components can be associated with pre- and post-conditions, i.e., a contract, that can be distributed to third-party developers. The framework ensures that if the components are compliant with their contracts, they can be safely integrated into the initial partial design without additional rework. As a result, FIDDle supports an iterative design process and guarantees correctness of the system at any step of development. We evaluated the effectiveness of FIDDle in supporting an iterative and incremental development of components using the K9 Mars Rover example developed at NASA Ames. This can be considered as an initial, yet substantive, validation of the approach in a realistic setting. We also assessed the scalability of FIDDle by comparing its efficiency with the classical model checkers implemented within the LTSA toolset. Results show that FIDDle scales as well as classical model checking as the number of the states of the components under development and their environments grow.

Software systems are usually formed by multiple components which interact with one another. In large systems, components themselves can be complex systems that need to be decomposed into multiple sub-components. Hence, system design must follow a systematic approach, based on a recursive decomposition strategy. This paper proposes a comprehensive verification-driven framework which provides support for designers during development. The framework supports hierarchical decomposition of components into sub-components through formal specification in terms of pre- and post-conditions as well as independent development, reuse and verification of sub-components.

We present design concepts, programming constructs, and automatic verification techniques to support the development of adaptive Wireless Sensor Network (WSN) software. WSNs operate at the interface between the physical world and the computing machine and are hence exposed to unpredictable environment dynamics. WSN software must adapt to these dynamics to maintain dependable and efficient operation. However, developers are left without proper support to develop adaptive functionality in WSN software. Our work fills this gap with three key contributions: (i) design concepts help developers organize the necessary adaptive functionality and understand their relations, (ii) dedicated programming constructs simplify the implementations, (iii) custom verification techniques allow developers to check the correctness of their design before deployment. We implement dedicated tool support to tie the three contributions, facilitating their practical application. Our evaluation considers representative WSN applications to analyze code metrics, synthetic simulations, and cycle-accurate emulation of popular WSN platforms. The results indicate that our work is effective in simplifying the development of adaptive WSN software; for example, implementations are provably easier to test and to maintain, the run-time overhead of our dedicated programming constructs is negligible, and our verification techniques return results in a matter of seconds.

Ubiquitous computing is resulting in a proliferation of cyber-physical systems that host or manage valuable physical and digital assets. These assets can be harmed by malicious agents through both cyber-enabled or physically-enabled attacks, particularly ones that exploit the often ignored interplay between the cyber and physical world. The explicit representation of spatial topology is key to supporting adaptive security policies. In this paper we explore the use of Bigraphical Reactive Systems to model the topology of cyber and physical spaces and their dynamics. We utilise such models to perform speculative threat analysis through model checking to reason about the consequences of the evolution of topological configurations on the satisfaction of security requirements. We further propose an automatic planning technique to identify an adaptation strategy enacting security policies at runtime to prevent, circumvent, or mitigate possible security requirements violations. We evaluate our approach using a case study concerned with countering insider threats in a building automation system.

We increasingly live in cyber-physical spaces -- spaces that are both physical and digital, and where the two aspects are intertwined. Such spaces are highly dynamic and typically undergo continuous change. Software engineering can have a profound impact in this domain, by defining suitable modeling and specification notations as well as supporting design-time formal verification. In this paper, we present a methodology and a technical framework which support modeling of evolving cyber-physical spaces and reasoning about their spatio-temporal properties. We utilize a discrete, graph-based formalism for modeling cyber-physical spaces as well as primitives of change, giving rise to a reactive system consisting of rewriting rules with both local and global application conditions. Formal reasoning facilities are implemented adopting logic-based specification of properties and according model checking procedures, in both spatial and temporal fragments. We evaluate our approach using a case study of a disaster scenario in a smart city.

Change has been recognized as the distinguishing feature that makes software different from any other human-produced artifacts. Initial reflections on the urgent and unavoidable need to master change date back to the 1970s. However, despite the continuous progress that characterized software technology since, in practice, software change is still often handled as an afterthought, in an ad hoc and unprincipled manner. Agile development methods have been proposed and are now widely adopted to accommodate change during development. Recent extensions to also include operation—known as DevOps—are increasingly and successfully adopted by industry. Still, principled and rigorous foundations that can be taught, practiced, and replicated systematically are lacking. This paper argues that change has to become a first-class concept and that the development tools used by engineers and the runtime environment supporting software execution should be structured in a way that naturally accommodates change. It also provides a perspective along which several research approaches that were investigated by the community in the past decade might be integrated and extended to make this vision become true. Two main change categories are identified—evolution and adaptation—along with the forces that drive them. The paper discusses when and how the developed software can be designed in a way that it can self-adapt. It also discusses how the software itself can cooperate with humans in-the-loop to help them in their design and development efforts. Finally, it outlines a roadmap of future work needed to progress in the direction of supporting and automating software change that would lead to dependable adaptation and evolution.

Modern component-based distributed software systems are increasingly required to offer non-stop service and thus their updates must be carried out at runtime. Different authors have already proposed solutions for the safe management of dynamic updates. Our contribution aims at improving their efficiency without compromising safety. We propose a new criterion, called version consistency, which defines when a dynamic update can be safely and efficiently applied to the components that execute distributed transactions. Version consistency ensures that distributed transactions be served as if they were operated on a single coherent version of the system despite possible concurrent updates. The paper presents a distributed algorithm for checking version consistency efficiently, formalizes the proposed approach by means of a graph transformation system, and verifies its correctness through model checking. The paper also presents ConUp, a novel prototype framework that supports the approach and offers a viable, concrete solution for the use of version consistency. Both the approach and ConUp are evaluated on a significant third-party application. Obtained results witness the benefits of the proposed solution with respect to both timeliness and disruption.

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval of the formula to be checked. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches.

Formal verification is used to establish the compliance of software and hardware systems with important classes of requirements. System compliance with functional requirements is frequently analyzed using techniques such as model checking, and theorem proving. In addition, a technique called quantitative verification supports the analysis of the reliability, performance, and other quality-of-service (QoS) properties of systems that exhibit stochastic behavior. In this paper, we extend the applicability of quantitative verification to the common scenario when the probabilities of transition between some or all states of the Markov models analyzed by the technique are unknown, but observations of these transitions are available. To this end, we introduce a theoretical framework, and a tool chain that establish confidence intervals for the QoS properties of a software system modelled as a Markov chain with uncertain transition probabilities. We use two case studies from different application domains to assess the effectiveness of the new quantitative verification technique. Our experiments show that disregarding the above source of uncertainty may significantly affect the accuracy of the verification results, leading to wrong decisions, and low-quality software systems.

Modern software-intensive systems often interact with an environment whose behavior changes over time, often unpredictably. The occurrence of changes may jeopardize their ability to meet the desired requirements. It is therefore desirable to design software in a way that it can self-adapt to the occurrence of changes with limited, or even without, human intervention. Self-adaptation can be achieved by bringing software models and model checking to run time, to support perpetual automatic reasoning about changes. Once a change is detected, the system itself can predict if requirements violations may occur and enable appropriate counter-actions. However, existing mainstream model checking techniques and tools were not conceived for run-time usage; hence they hardly meet the constraints imposed by on-the-fly analysis in terms of execution time and memory usage. This paper addresses this issue and focuses on perpetual satisfaction of non-functional requirements, such as reliability or energy consumption. Its main contribution is the description of a mathematical framework for run-time efficient probabilistic model checking. Our approach statically generates a set of verification conditions that can be efficiently evaluated at run time as soon as changes occur. The proposed approach also supports sensitivity analysis, which enables reasoning about the effects of changes and can drive effective adaptation strategies.

Modern software systems are increasingly required to run for a long time and deliver uninterrupted service. Their requirements or their environments, however, may change. Therefore, these systems must be updated dynamically, at run-time. Typical examples can be found in manufacturing, transportation, or space applications, where stopping the system to deploy updates can be difficult, costly, or simply not possible. In previous work we proposed a model-driven approach that uses automatically synthesized finite-state controllers from scenario-based assume/guarantee specifications to safely and efficiently dynamically update the system. In this paper we describe an execution infrastructure of this approach, which allows us to execute and deploy newly synthesized dynamically updating controllers on embedded devices. We present a prototype implementation in Java for Lego Mind storms robots. This experience gained can lead to a systematic approach to implement dynamic updates in the aforementioned critical software-intensive systems.

This paper presents Ariadne, a tool for engineering topology aware adaptive security for cyber-physical systems. It allows security software engineers to model security requirements together with the topology of the operational environment. This model is then used at runtime to perform speculative threat analysis to reason about the consequences that topological changes arising from the movement of agents and assets can have on the satisfaction of security requirements. Our tool also identifies an adaptation strategy that applies security controls when necessary to prevent potential security requirements violations.

Constraint solution reuse is an effective approach to save the time of constraint solving in symbolic execution. Most of the existing reuse approaches are based on syntactic or semantic equivalence of constraints. For example, the Green framework can reuse constraints which have different representations but are semantically equivalent, through canonizing constraints into syntactically equivalent normal forms. KLEE reuses constraints based on subset/superset querying. However, both equivalence-based approach and subset/superset-based approach cannot cover some kinds of reuse where atomic constraints are not equivalent. Our approach, called GreenTrie, is an extension to the Green framework, which supports constraint reuse based on the logical implication relations among constraints. GreenTrie provides a component, called L-Trie, which stores constraints and solutions into tries, indexed by an implication partial order graph of constraints. L-Trie is able to carry out logical reduction and logical subset and superset querying for given constraints, to check for reuse of previously solved constraints. We report the results of an experimental assessment of GreenTrie against the original Green framework and the KLEE approach, which shows that our extension achieves better reuse of constraint solving result and saves significant symbolic execution time.

Modern iterative and incremental software development relies on continuous testing. The knowledge of test-to-code traceability links facilitates test-driven development and improves software evolution. Previous research identified traceability links between test cases and classes under test. Though this information is helpful, a finer granularity technique can provide more useful information beyond the knowledge of the class under test. In this paper, we focus on Java classes that instantiate stateful objects and propose an automated technique for precise detection of the focal methods under test in unit test cases. Focal methods represent the core of a test scenario inside a unit test case. Their main purpose is to affect an object's state that is then checked by other inspector methods whose purpose is ancillary and needs to be identified as such. Distinguishing focal from other (non-focal) methods is hard to accomplish manually. We propose an approach to detect focal methods under test automatically. An experimental assessment with real-world software shows that our approach identifies focal methods under test in more than 85% of cases, providing a ground for precise automatic recovery of test-to-code traceability links.

Summary Modern software systems are increasingly built by integrating different services implemented by independent organizations and offered in an open service marketplace. In such environment, multiple providers may compete with each other by publishing services that provide the same functionality, and export the same interface, but differ in the offered QoS and in particular in the offered performance. Clients and service integrators may therefore dynamically select the most efficient services that satisfy their requirements among the competing alternatives. Service selection may be performed by clients by following different strategies, which may ultimately affect the overall quality of service invocations. In this paper, we address the problem of analyzing and comparing different service selection strategies based on a framework that supports performance estimates. We report on quantitative analyses through simulations, highlighting advantages and limitations of each strategy. Copyright © 2014 John Wiley & Sons, Ltd.

We present programming abstractions for implementing adaptive Wireless Sensor Network (WSN) software. The need for adaptability arises in WSNs because of unpredictable environment dynamics, changing requirements, and resource scarcity. However, after about a decade of research in WSN programming, developers are still left with no dedicated support. To address this issue, we bring concepts from Context-Oriented Programming (COP) down to WSN devices. Contexts model the situations that WSN software needs to adapt to. Using COP, programmers use a notion of layered function to implement context-dependent behavioral variations of WSN code. To this end, we provide language-independent design concepts to organize the context-dependent WSN operating modes, decoupling the abstractions from their concrete implementation in a programming language. Our own implementation, called CONESC, extends nesC with COP constructs. Based on three representative applications, we show that CONESC greatly simplifies the resulting code and yields increasingly decoupled implementations compared to nesC. For example, by model-checking every function in either implementations, we show a ~50% reduction in the number of program states that programmers need to deal with, indicating easier debugging. In our tests, this comes at the price of a maximum 2.5% (4.5%) overhead in program (data) memory.

Many modern user-intensive applications, such as Web applications, must satisfy the interaction requirements of thousands if not millions of users, which can be hardly fully understood at design time. Designing applications that meet user behaviors, by efficiently supporting the prevalent navigation patterns, and evolving with them requires new approaches that go beyond classic software engineering solutions. We present a novel approach that automates the acquisition of user-interaction requirements in an incremental and reflective way. Our solution builds upon inferring a set of probabilistic Markov models of the users' navigational behaviors, dynamically extracted from the interaction history given in the form of a log file. We annotate and analyze the inferred models to verify quantitative properties by means of probabilistic model checking. The paper investigates the advantages of the approach referring to a Web application currently in use.

Developers spend a significant portion of their time understanding and learning the correct usage of the APIs of libraries they want to integrate in their projects. However, learning how to effectively use APIs is complex and time consuming. Code recommendation systems play a crucial role facilitating developers in this task by providing to them relevant examples while they code. This paper proposes a novel approach to code recommendation in which code examples are automatically obtained by mining and manipulating unit tests. In this paper we discuss the theoretical and practical implications that underpin this idea. The discussion leads to a series of fascinating research challenges that we organized in a research agenda.

Adaptive security systems aim to protect critical assets in the face of changes in their operational environment. We have argued that incorporating an explicit representation of the environment's topology enables reasoning on the location of assets being protected and the proximity of potentially harmful agents. This paper proposes to engineer topology aware adaptive security systems by identifying violations of security requirements that may be caused by topological changes, and selecting a set of security controls that prevent such violations. Our approach focuses on physical topologies; it maintains at runtime a live representation of the topology which is updated when assets or agents move, or when the structure of the physical space is altered. When the topology changes, we look ahead at a subset of the future system states. These states are reachable when the agents move within the physical space. If security requirements can be violated in future system states, a configuration of security controls is proactively applied to prevent the system from reaching those states. Thus, the system continuously adapts to topological stimuli, while maintaining requirements satisfaction. Security requirements are formally expressed using a propositional temporal logic, encoding spatial properties in Computation Tree Logic (CTL). The Ambient Calculus is used to represent the topology of the operational environment - including location of assets and agents - as well as to identify future system states that are reachable from the current one. The approach is demonstrated and evaluated using a substantive example concerned with physical access control.

Autonomous drones are a powerful new breed of mobile sensing platform that can greatly extend the capabilities of traditional sensing systems. Unfortunately, it is still non-trivial to coordinate multiple drones to perform a task collaboratively. We present a novel programming model called team-level programming that can express collaborative sensing tasks without exposing the complexity of managing multiple drones, such as concurrent programming, parallel execution, scaling, and failure recovering. We create the Voltron programming system to explore the concept of team-level programming in active sensing applications. Voltron offers programming constructs to create the illusion of a simple sequential execution model while still maximizing opportunities to dynamically re-task the drones as needed. We implement Voltron by targeting a popular aerial drone platform, and evaluate the resulting system using a combination of real deployments, user studies, and emulation. Our results indicate that Voltron enables simpler code and produces marginal overhead in terms of CPU, memory, and network utilization. In addition, it greatly facilitates implementing correct and complete collaborative drone applications, compared to existing drone programming systems.

In this paper, we focus on the reliability and availability analysis of Web service (WS) compositions, orchestrated via the Business Process Execution Language (BPEL). Starting from the failure profiles of the services being composed, which take into account multiple possible failure modes, latent errors, and propagation effects, and from a BPEL process description, we provide an analytical technique for evaluating the composite process' reliability-availability metrics. This technique also takes into account BPEL's advanced composition features, including fault, compensation, termination, and event handling. The method is a design-time aid that can help users and third party providers reason, in the early stages of development, and in particular during WS selection, about a process' reliability and availability. A non-trivial case study in the area of travel management is used to illustrate the applicability and effectiveness of the proposed approach.

Modern software systems are often characterized by uncertainty and changes in the environment in which they are embedded. Hence, they must be designed as adaptive systems. We propose a framework that supports adaptation to non-functional manifestations of uncertainty. Our framework allows engineers to derive, from an initial model of the system, a finite state automaton augmented with probabilities. The system is then executed by an interpreter that navigates the automaton and invokes the component implementations associated to the states it traverses. The interpreter adapts the execution by choosing among alternative possible paths of the automaton in order to maximize the system's ability to meet its non-functional requirements. To demonstrate the adaptation capabilities of the proposed approach we implemented an adaptive application inspired by an existing worldwide distributed mobile application and we discussed several adaptation scenarios.

Conventional formal verification techniques rely on the assumption that a system's specification is completely available so that the analysis can say whether or not a set of properties will be satisfied. On the contrary, modern development lifecycles call for agileincremental and iterativeapproaches to tame the boosting complexity of modern software systems and reduce development risks. We focus here on requirements verification performed in the early exploratory stages on high-level models and we discuss how this can be integrated into an agile approach. We present a new technique to model-check incomplete high-level specifications against formally specified requirements. We do this in the context of incomplete hierarchical Statecharts, verified against a variation of CTL properties. Our approach supports step-wise specification and refinement verification. Verification can be incremental, that is alternative refinements may be separately explored and verification is only replayed for the modified parts. The results are presented by introducing the formalisms, the model-checking algorithm, and the tool we have implemented.

We present our ongoing work on the design of macroprogramming abstractions to program sensing and actuating applications using robot swarms. Robots can sample the environment and act on it where no other sensor can reach, e.g., to monitor the environment at altitude with aerial robots. Programming the individual behavior of multiple coordinating robots is difficult. We design LiftOff, a macroprogramming abstraction that allows to program robot swarms collectively, by creating the illusion of a single computing device that occupies the entire physical space of interest. We achieve this by giving variables and values in a programming language a spatial semantics. In LiftOff, values may be associated to a location, and programmers use the same variable to access different values at different locations, sparing the need to manually create a mapping from variables to spatial values. LiftOff applications execute synchronously or based on lazy evaluation. The former allows precise program analysis, e.g., using model checking, whilst the latter potentially executes faster. In this paper, we report on LiftOff's initial design and prototypes.

Self-adaptive software has become increasingly important to address the new challenges of complex computing systems. To achieve adaptation, software must be designed and implemented by following suitable criteria, methods, and strategies. Past research has been mostly addressing adaptation by developing solutions at the software architecture level. This work, instead, focuses on finer-grain programming language-level solutions. We analyze three main linguistic approaches: metaprogramming, aspect-oriented programming, and context-oriented programming. The first two are general-purpose linguistic mechanisms, whereas the third is a specific and focused approach developed to support context-aware applications. This paradigm provides specialized language-level abstractions to implement dynamic adaptation and modularize behavioral variations in adaptive systems. The article shows how the three approaches can support the implementation of adaptive systems and compares the pros and cons offered by each solution.

This paper describes a novel model for the service selection problem of workflow-based applications in the context of self-managing situated computing. In such systems, the execution environment includes different types of devices, from remote servers to personal notebooks, smartphones, and wireless sensors, which build an infrastructure that can dynamically change both its physical and logical architecture at runtime. We assume that workflows are defined abstractly; i.e., they invoke abstract services whose concrete counterparts can be selected dynamically. We also assume that concrete service implementations may possibly migrate on the nodes of the infrastructure. The selection problem we address is framed as an optimization problem of the quality of service (QoS), which evaluates at runtime the optimal binding to concrete services as well as the tradeoff between the remote execution of software fragments and their dynamic deployment on local nodes of the computational environment. The final deployment takes into account quality of service constraints, the capabilities of the physical devices involved, including their performance and energy consumption, and the characteristics of the networking links connecting them.

Specification patterns have proven to help developers to state precise system requirements, as well as formalize them by means of dedicated specification languages. Most of the past work has focused its applicability area to the specification of concurrent and real-time systems, and has been limited to a research setting. In this paper we present the results of our study on specification patterns for service-based applications (SBAs). The study focuses on industrial SBAs in the banking domain. We started by performing an extensive analysis of the usage of specification patterns in published research case studies - representing almost ten years of research in the area of specification, verification, and validation of SBAs. We then compared these patterns with a large body of specifications written by our industrial partner over a similar time period. The paper discusses the outcome of this comparison, indicating that some needs of the industry, especially in the area of requirements specification languages, are not fully met by current software engineering research.

Contracts are a popular declarative specification technique to describe the behavior of stateful components in terms of pre/post conditions and invariants. Since each operation is specified separately in terms of an abstract implementation, it may be hard to understand and validate the resulting component behavior from contracts in terms of method interactions. In particular, properties expressed through algebraic axioms, which specify the effect of sequences of operations, require complex theorem proving techniques to be validated. In this paper, we propose an automatic small-scope based approach to synthesize incomplete behavioral abstractions for contracts expressed in the JFSL notation. The proposed abstraction technique enables the possibility to check that the contract behavior is coherent with behavioral properties expressed as axioms of an algebraic specifications. We assess the applicability of our approach by showing how the synthesis methodology can be applied to some classes of contract-based artifacts like specifications of data abstractions and requirement engineering models.

We present Spy@Runtime, a tool to infer and work with behavior models. Spy@Runtime generates models through a dynamic black box approach and is able to keep them updated with observations coming from actual system execution. We also show how to use models describing the protocol of interaction of a software component to detect and report functional changes as soon as they are discovered. Monitoring functional properties is particularly useful in an open environment in which there is a distributed ownership of a software system. Parts of the system may be changed independently and therefore it becomes necessary to monitor the component's behavior at run time.

We present the workflow language DSOL, its runtime system and the tools available to support the development of dynamic service orchestrations. DSOL aims at supporting dynamic, self-managed service compositions that can adapt to changes occurring at runtime.

In this demo we present SelfMotion: a declarative language and a run-time system conceived to support the development of adaptive, mobile applications, built as compositions of ad-hoc components, existing services and third party applications. The advantages of the approach and the adaptive capabilities of SelfMotion are demonstrated in the demo by designing and executing a mobile application inspired by an existing, worldwide distributed, mobile application.

Abstract Modern software systems are increasingly requested to be adaptive to changes in the environment in which they are embedded. Moreover, adaptation often needs to be performed automatically, through self-managed reactions enacted by the application at run time. Off-line, human-driven changes should be requested only if self-adaptation cannot be achieved successfully. To support this kind of autonomic behavior, software systems must be empowered by a rich run-time support that can monitor the relevant phenomena of the surrounding environment to detect changes, analyze the data collected to understand the possible consequences of changes, reason about the ability of the application to continue to provide the required service, and finally react if an adaptation is needed. This paper focuses on non-functional requirements, which constitute an essential component of the quality that modern software systems need to exhibit. Although the proposed approach is quite general, it is mainly exemplified in the paper in the context of service-oriented systems, where the quality of service (QoS) is regulated by contractual obligations between the application provider and its clients. We analyze the case where an application, exported as a service, is built as a composition of other services. Non-functional requirements—such as reliability and performance—heavily depend on the environment in which the application is embedded. Thus changes in the environment may ultimately adversely affect QoS satisfaction. We illustrate an approach and support tools that enable a holistic view of the design and run-time management of adaptive software systems. The approach is based on formal (probabilistic) models that are used at design time to reason about dependability of the application in quantitative terms. Models continue to exist at run time to enable continuous verification and detection of changes that require adaptation.

Symbolic program manipulation plays a key role in program comprehension and verification. Logic formulae are used to represent the program' s state and transformation rules describe the effect of statement executions on the program's state. A well-known problem arises in the case of loops, since the number of iterations is generally unknown. The effect of a loop is therefore abstracted into a loop invariant, whose derivation cannot in general be automated and requires human ingenuity. In this paper, we present a preliminary approach that in tegrates genetic programming into the synthesis of invariant formula that describes the behavior of a loop. We present a specific representation of formulae that works well with loops manipulating arrays. The technique has been validated with a set of relevant examples with increasing complexity. The preliminary results are promising and show the feasibility of our approach.

Software projects have crossed seas and continents looking for talented developers, moving from local developments to geographically distributed projects. This paper presents a case study analyzing the effect of distribution and time zones on communication in distributed projects. The study was performed in a university course during two semesters, where students developed projects jointly with teams located in ten different countries in South America, Europe, and Asia. The study compares the results of the projects distributed in two locations with projects distributed in three locations. It also analyzes projects in different time zone ranges. The initial results show that the amount of communication in projects distributed in two locations is bigger than the communication in projects distributed in three locations. We also found that projects in closer time zones have more communication than projects in farther time zones. Furthermore, we analyze the reply time for e-mails of projects distributed in different time zones, and discuss the challenges faced by the students during these projects.

Unpredictable changes continuously affect software systems and may have a severe impact on their quality of service, potentially jeopardizing the system's ability to meet the desired requirements. Changes may occur in critical components of the system, clients' operational profiles, requirements, or deployment environments.

This paper investigates a novel approach to derive self-adaptive software by automatically modifying the model of the application using a control-theoretical approach. Self adaptation is achieved at the model level to assure that the model-which lives alongside the application at run-time- continues to satisfy its reliability requirements, despite changes in the environment that might lead to a violation. We assume that the model is given in terms of a Discrete Time Markov Chain (DTMC). DTMCs can express reliability concerns by modeling possible failures through transitions to failure states. Reliability requirements may be expressed as reachability properties that constrain the probability to reach certain states, denoted as failure states. We assume that DTMCs describe possible variant behaviors of the adaptive system through transitions exiting a given state that represent alternative choices, made according to certain probabilities. Viewed from a control-theory standpoint, these probabilities correspond to the input variables of a controlled system-i.e., in the control theory lexicon, "control variables". Adopting the same lexicon, such variables are continuously modified at run-time by a feedback controller so as to ensure continuous satisfaction of the requirements despite disturbances, i.e., changes in the environment. Changes at the model level may then be automatically transferred to changes in the running implementation. The approach is methodologically described by providing a translation scheme from DTMCs to discrete-time dynamic systems, the formalism in which the controllers are derived. An initial empirical assessment is described for a case study. Conjectures for extensions to other models and other requirements.

Assurances for Self-Adaptive Systems (ASAS) is a workshop that will bring together researchers to discuss software engineering aspects of self-adaptive systems, including methods, architectures, languages, algorithms, techniques, and tools that can be used to support assurances in self-adaptive system development. ASAS is intended as a complement to the efforts started a while ago at the successful FSE workshop series on Self-Healing Systems (WOSS), or the Software Engineering for Adaptive and Self-Managing Systems (SEAMS) symposium. However, in contrast with those events, ASAS is focused on the collection, storage, and analysis of evidence for the provision of assurances that a self-adaptive software system is able to behave functionally and non-functionally according to its specification.

There is an increasing demand for the runtime reconfiguration of distributed systems in response to changing environments and evolving requirements. Reconfiguration must be done in a safe and low-disruptive way. In this paper, we propose version consistency of distributed transactions as a safe criterion for dynamic reconfiguration. Version consistency ensures that distributed transactions be served as if there were operating on a single coherent version of the system despite possible reconfigurations that may happen meanwhile. The paper also proposes a distributed algorithm to maintain dynamic dependences between components at architectural level and enable low-disruptive version-consistent dynamic reconfigurations. An initial assessment through simulation shows the benefits of the proposed approach with respect to timeliness and low degree of disruption.

In this paper, we describe how probabilistic model checking techniques and tools can be used to verify non-functional properties of different configurations of a software product line. We propose a model-based approach that enables software engineers to assess their design solutions in the early stages of development. Furthermore, we discuss how verification time can surprisingly be reduced by applying parametric model checking instead of classic model checking, and show that the approach can be effective in practice.

The Publish-Subscribe (P/S) communication paradigm fosters high decoupling among distributed components. This facilitates the design of dynamic applications, but also impacts negatively on their verification, making it difficult to reason on the overall federation of components. In addition, existing P/S infrastructures offer radically different features to the applications, e.g., in terms of message reliability. This further complicates the verification as its outcome depends on the specific guarantees provided by the underlying P/S system. Although model checking has been proposed as a tool for the verification of P/S architectures, existing solutions overlook many characteristics of the underlying communication infrastructure to avoid state explosion problems. To overcome these limitations, the Loupe domain-specific model checker adopts a different approach. The P/S infrastructure is not modeled on top of a general-purpose model checker. Instead, it is embedded within the checking engine, and the traditional P/S operations become part of the modeling language. In this paper, we describe Loupe's design and the dedicated state abstractions that enable accurate verification without incurring state explosion problems. We also illustrate our use of state-of-the-art software verification tools to assess some key functionality in Loupe's current implementation. A complete case study shows how Loupe eases the verification of P/S architectures. Finally, we quantitatively compare Loupe's performance against alternative approaches. The results indicate that Loupe is effective and efficient in enabling accurate verification of P/S architectures.

Getting insight into different aspects of source code artifacts is increasingly important – yet there is little empirical research using large bodies of source code, and subsequently there are not much statistically significant evidence of common patterns and facts of how programmers write source code. We pose 32 research questions, explain rationale behind them, and obtain facts from 2,080 randomly chosen Java applications from Sourceforge. Among these facts we find that most methods have one or zero arguments or they do not return any values, few methods are overridden, most inheritance hierarchies have the depth of one, close to 50 % of classes are not explicitly inherited from any classes, and the number of methods is strongly correlated with the number of fields in a class. Categories and Subject Descriptors

Nowadays requirements related to quality attributes such as performance, reliability, safety and security are often considered the most important requirements for software development projects. To reason about these quality attributes different stochastic models can be used. These models enable probabilistic verification as well as quantitative prediction at design time. On the other hand, these models could be also used to perform runtime adaptation in order to achieve certain quality goals. This workshop aims to provide a forum for researchers in these areas that should help with the adoption of quantitative stochastic models into general software development processes.

Modern software applications increasingly live in an open world, characterized by continuous change in the environment in which they are situated and in the requirements they have to meet. Continuous changes occur autonomously and unpredictably, in a way that can hardly be predicted (and taken care of) by software engineers, as the application is designed. As a consequence, changes are out of control of the running application, which cannot handle them. On the other hand, there is an increasing demand for software solutions that can easily evolve and dynamically adapt their behavior to provide continuous service as changes occur. This is especially needed when systems must be perpetually running and cannot be changed off-line. Hereafter I focus on environment changes that may affect an application. This may include changes in the way people interact with the system or changes in the external components, which offer services upon which the currently developed application relies. Moreover, I will mostly focus on quantitatively stated requirements that express nonfunctional properties of an application, such as performance or reliability. Because of the uncertainty that characterizes open-world settings, requirements should be expressed in probabilistic terms. I will argue that models at run-time are needed to support continuous verification. Furthermore, I will discuss why continuous verification is needed to support an on-line update of the application's model, which-in turn-may support formal approaches to software evolution. I focus on system requirements that are stated in quantitative and probabilistic terms, such as reliability and performance requirements. I also focus on the use of Markov models, which may be used at design-time to verify satisfaction of the requirements, based on assumptions on the behavior of the environment. Assuming, for instance, that the whole system is modeled as a Discrete-Time Markov Chain, probabilities attached to transitions may be used to represent user profiles (e.g., the probability that a certain operation is invoked by the user). They may also represent failure rates of external services used by the application, or performance figures about their response time. Once the model is built at design-time, one can state properties that the system should satisfy and use the model to check if such properties are verified, for example through automated probabilistic model checking (e.g. By monitoring the environment at run-time, we collect data that correspond to the actual external behaviors that may affect the application. For example, we monitor user interactions as well as the real failure rates and response time of external components. The collected data may be analyzed by a machine learning process, which may produce updated estimates for the probabilities attached to the transitions of the DTMC model of the application. As the model is updated with current values of the parameters, it can be run to check if the desired properties of the application, which were proved to hold at development time, still hold at run-time. In case they do, no action is in general required. Instead, if a violation occurs, suitable recovery actions must be put in place. One may distinguish here between two cases that characterize a violation of the desired global properties. The violation may correspond to a predicted future failure of the running system or it may correspond to an actually experienced failure. The former case should trigger a preventive recovery procedure, whose success may assure that no failure will be experienced in practice. The latter case instead triggers a recovery procedure that tries to compensate the effect of the experienced failure. The view discussed here is currently being investigated in all its facets by the DeepSE Group at Politecnico di Milano. Moreover a prototype environment (called KAMI) is being developed to support both development-time modeling and analysis and run-time model evolution. In turn, run-time verification supports adaptation, both to prevent failures and to recover from them. Future work will consolidate the current approach and will focus on several unresolved issues, such as understanding and supporting run-time adaptation strategies (a preliminary approach is described in, and devising further approaches to run-time verification that may lead to time-efficient analysis at run-time without the need for using time-expensive model checkers. This-in turn-would enable reactions that may satisfy stringent time constraints.

Modern software systems are increasingly built out of services that are developed, deployed, and operated by independent organizations, which expose them for use by potential clients. Services may be directly invoked by clients. They may also be composed by service integrators, who in turn expose the composite artifact as a new service. Continuous change is typical of this world. Providers may change services and the deployment infrastructure to meet continuously changing requirements and be more competitive. Clients may change their operational profiles. Changes have a severe impact on the quality of services.

REMAN is a reputation management infrastructure for composite Web services. It supports the aggregation of client feedback on the perceived QoS of external services, using reputation mechanisms to build service rankings. Changes in rankings are pro-actively notified to composite service clients to enable self-tuning properties in their execution.

Models can help software engineers to reason about design-time decisions before implementing a system. This paper focuses on models that deal with non-functional properties, such as reliability and performance. To build such models, one must rely on numerical estimates of various parameters provided by domain experts or extracted by other similar systems. Unfortunately, estimates are seldom correct. In addition, in dynamic environments, the value of parameters may change over time. We discuss an approach that addresses these issues by keeping models alive at run time and feeding a Bayesian estimator with data collected from the running system, which produces updated parameters. The updated model provides an increasingly better representation of the system. By analyzing the updated model at run time, it is possible to detect or predict if a desired property is, or will be, violated by the running implementation. Requirement violations may trigger automatic reconfigurations or recovery actions aimed at guaranteeing the desired goals. We illustrate a working framework supporting our methodology and apply it to an example in which a Web service orchestrated composition is modeled through a discrete time Markov chain. Numerical simulations show the effectiveness of the approach.

This paper describes an approach (SPY) to recovering the specification of a software component from the observation of its run-time behavior. It focuses on components that behave as data abstractions. Components are assumed to be black boxes that do not allow any implementation inspection. The inferred description may help understand what the component does when no formal specification is available. SPY works in two main stages. First, it builds a deterministic finite-state machine that models the partial behavior of instances of the data abstraction. This is then generalized via graph transformation rules. The rules can generate a possibly infinite number of behavior models, which generalize the description of the data abstraction under an assumption of ldquoregularityrdquo with respect to the observed behavior. The rules can be viewed as a likely specification of the data abstraction. We illustrate how SPY works on relevant examples and we compare it with competing methods.

We focus on non-functional requirements for applications offered by service integrators; i.e., software that delivers service by composing services, independently developed, managed, and evolved by other service providers. In particular, we focus on requirements expressed in a probabilistic manner, such as reliability or performance. We illustrate a unified approach-a method and its support tools-which facilitates reasoning about requirements satisfaction as the system evolves dynamically. The approach relies on run-time monitoring and uses the data collected by the probes to detect if the behavior of the open environment in which the application is situated, such as usage profile or the external services currently bound to the application, deviates from the initially stated assumptions and whether this can lead to a failure of the application. This is achieved by keeping a model of the application alive at run time, automatically updating its parameters to reflect changes in the external world, and using the model's predictive capabilities to anticipate future failures, thus enabling suitable recovery plans.

The dependability of composite services is largely affected by their constituent Web services. Composite services have to operate in an open and dynamically changing environment in order to leverage the best performing services available at the moment. Hence, there is the need for an efficient mechanism to provide reliable service rankings. In this paper we present a novel, generic, and customizable reputation infrastructure to automatically and transparently monitor the execution of composite services, taking both functional and non-functional properties into account. The experienced Web service quality-of-service is communicated to a configurable reputation mechanism that publishes service rankings. Our reputation infrastructure supports notifications upon changes in service reputation, enabling self-tuning and self-healing properties in the execution of composite services. We implemented our architecture using standard technologies, such as BPEL and JavaEE. Performance measurements show that our infrastructure causes only moderate overhead.

The paper presents a novel approach based on Bogor for the accurate verification of applications based on Publish- Subscribe infrastructures. Previous efforts adopted standard model checking techniques to verify the application behavior, but they introduce strong simplifications on the underlying infrastructure to cope with the state space explosion problem and make automatic verification feasible. Instead of building on top of existing model checkers, our proposal embeds the asynchronous communication mechanisms of Publish-Subscribe infrastructures within Bogor. This way, Publish-Subscribe primitives become part of the specification language as additional, domain-specific, constructs. Accurate models become feasible without incurring in state space explosion problems, thus enabling the automated verification of applications on top of realistic communication infrastructures.

Web service based applications are expected to live in dynamically evolving settings. At run-time, services may undergo changes that could modify their expected behavior. Because of such intrinsic dynamic nature, applications should be designed by adhering to the principles of design- by-contract. Run-time monitoring is needed to check that the contract between service providers and service users is fulfilled while the collaboration is in place. We describe a language to specify the expected functional and non-functional requirements that a service provider should fulfill. The language (timed WSCoL) is a temporal extension of a previous proposal (WSCoL). We also illustrate the architecture of a run-time analyzer that checks timed WSCoL properties. Should such properties be disproved during execution, appropriate recovery and reconfiguration actions may be put in place.

The Doctoral Symposium of ESCE/FSE aims at creating a forum for PhD students working in the area of software engineering to present and discuss their research goals, methods, and preliminary results with senior researchers from the software engineering community, in a constructive and friendly atmosphere. Besides providing a setting whereby students receive feedback on their research and guidance on future directions from the doctoral symposium panel, the creation of a supportive community of scholars and a spirit of collaborative research, also through interaction of the participants with other researchers at the main conference.

No abstract available.

The increasing diffusion of ubiquitous communication infrastructures and physical active objects-like sensors and smart tags-is motivating the integration of these devices into advanced distributed systems. The novelty of these technologies has imposed a "code and fix" approach; only a few methodologies have been developed to address the integration of heterogeneous technologies to provide the user with sophisticated and flexible abstractions of real world objects. To this end, the paper proposes the first results of a model-driven approach for the development of applications based on heterogeneous physical active objects. We propose a metamodel and a framework for automatic code generation based on Jini. The approach is exemplified on a simple case study in the domain of advanced logistics.

Summary form only given. Traditional software development is based on the closed-world assumption that the boundary between system and environment is known and unchanging. However, this assumption no longer works within today's unpredictable open-world settings, which demands techniques that let software react to changes by self-organizing its structure and self-adapting its behavior

Recent advances in wireless networks enable decentralized cooperative and nomadic work scenarios where mobile users can interact in performing some tasks without being permanently online. Scenarios where connectivity is transient and the network topology may change dynamically are considered. Connectivity among nodes does not require the support offered by a permanent infrastructure but may rely on ad hoc networking facilities. In this paper, a scenario in which a nomadic group of software engineers cooperate in developing an application is investigated. The proposed solution, however, is not software process specific but holds for other cases where shared documents are developed cooperatively by a number of interacting nomadic partners. Support tools for these groups are normally based on a client-server architecture, which appears to be unsuitable in highly dynamic environments. Peer-to-peer solutions, which do not rely on services provided by centralized servers, look more promising. This paper presents a fully decentralized cooperative infrastructure centered around peer-to-peer versioning system (PeerVerSy), a configuration management tool based on a peer-to-peer architecture, which supports cooperative services even when some of the collaborating nodes are offline. Some preliminary experiences gained from its use in a teaching environment are also discussed

We discuss the technical skills that a software engineer should possess. We take the viewpoint of a school of engineering and put the software engineer's education in the wider context of engineering education. We stress both the common aspects that crosscut all engineering fields and the specific issues that pertain to software engineering. We believe that even in a continuously evolving field like software, education should provide strong and stable foundations based on mathematics and science, emphasize the engineering principles, and recognize the stable and long-lasting design concepts. Even though the more mundane technological solutions cannot be ignored, the students should be equipped with skills that allow them to understand and dominate the evolution of technology.

editorial Free Access Share on Editorial Editor: Carlo Ghezzi View Profile Authors Info & Claims ACM Transactions on Software Engineering and MethodologyVolume 14Issue 2April 2005 pp 119–123https://doi.org/10.1145/1061254.1061255Published:01 April 2005Publication History 0citation567DownloadsMetricsTotal Citations0Total Downloads567Last 12 Months8Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

No abstract available.

Service-based approaches are widely used to integrate heterogenous systems. Web services allow for the definition of highly dynamic systems where components (services) can be discovered and QoS parameters negotiated at run-time. This justifies the need for monitoring service compositions at run-time. Research on this issue, however, is still in its infancy.

No abstract available.

In this paper we describe a configuration management tool suitable for the untethered scenarios typical in a mobile environment. The scenario envisions a number of homogeneous peers that are able to provide the same services, disconnect frequently from the net, and perform part of their work while disconnected. In these contexts the absence of a host is not the exceptional case, but rather the normal behavior. Thus, a traditional architecture based on a central repository exposes the system to failures when the server is unavailable. Instead, we build our system on a peer-to-peer middleware able to provide the abstraction of global virtual data structure, i.e., a data structure composed by all the data actually connected in a given instant. Thanks to this, we can exploit the service provided by the network even if relevant hosts are disconnected.

Safety critical systems require to be highly reliable and thus special care is taken when verifying them in order to increase the confidence in their behavior. This paper addresses the problem of formal verification of safety critical systems by providing empirical evidence of the practical applicability of symbolic execution and of its usefulness for checking safety-related properties. In this paper, symbolic execution is used for building an operational model of the software on which safety properties, expressed by means of a Path Description Language (PDL), can be assessed.

First Page of the Article""

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development and, therefore, has been formally defined. The structuring mechanisms in ASTRAL allow one to build modularized specifications of complex systems with layering. A real-time system is modeled by a collection of state machine specifications and a single global specification. This paper discusses the rationale of ASTRAL's design. ASTRAL's specification style is illustrated by discussing a telephony example. Composability of one or more ASTRAL system specifications is also discussed by the introduction of a composition section, which provides the needed information to combine two or more ASTRAL system specifications.

Most modern business activities are carried out by a combination of computerized tools and human agents. Typical examples are engineering design activities, office procedures, and banking systems. All these human-centered systems are characterized by the interaction among people, and between people and computerized tools. This interaction defines a process, whose effectiveness is essential to ensure the quality of the delivered products and/or services. To support these systems, process-centered environments and workflow management systems have been recently developed. They can be collectively identified with the term process technology . This technology is based on the explicit definition of the process to be followed (the process model ). The model specifies the kind of support that has to be provided to human agents. An essential property that process technology mut exhibit is the ability of tolerating, controlling, and supporting deviations and inconsistencies of the real-world behaviors with respect to the proocess model. This is necessary to provide consistent and effective support to the human-centered system, still maintaining a high degree of flexibility and adaptability to the evolving needs, preferences, an expertise of the the human agents. This article presents a formal framework to characterize the interaction between a human-centered system and its automated support. It does not aim at introducing a new language or system to describe processes. Rather, it aims at identifying the basic properties and features that make it possible to formally define the concepts of inconsistency and deviation. This formal framework can then be used to compare existing solutions and guide future research work.

A fundamental problem in software processes is how the mintrinsic rigidity of a predejined (formal) model can be reconciled with the need for flexibility, change, and evolution.We therefore distinguish between software processes, as specified in a process description, and their actual performance by humans.Further, we claim that the two inevitably diverge, and thus it is necessary to provide means to reconcile them.We present a preliminary exploration into the problem.In particular, we illustrate how a temporal logic-based approach can be used to capture and tolerate some deviations from the process description during execution.We present a simple process language (LATIN), and its prototype environment (SENTINEL), in which these ideas are currently experimented.1

We describe how formal specifications given in terms of a high-level timed Petri net formalism (TB nets) can be analyzed to check the temporal properties of bounded invariance (the systems stays in a given state until time τ) and bounded response (the system will enter a given state within time τ). In particular, we concentrate on specifications given in a hierarchical, top-down manner, where one specification level refines a more abstract level.

Process modeling is a rather young and very active research area. During the last few years, new languages and methods have been proposed to describe software processes. In this paper we try to clarify the issues involved in software process modeling and identify the main approaches. We start by motivating the use of process modeling and its main objectives. We then propose a list of desirable features for process languages. The features are grouped as either already provided by languages from other fields or as specific features of the process domain. Finally, we review the main existing approaches and propose a classification scheme.

Abstract Specifications of information systems applications are often based on the use of entity‐relationship (ER) and data‐flow diagrams (DFD), which cover, respectively, the conceptual modelling of data and funtions. This paper introduces VLP: an executable visual language for formal specifications and prototyping which integrates ER and DFD diagrams in a semantically rigorous and clear way. Unlike existing commercial products (so‐called CASE tools), which can support good‐quality documentation, simple forms of consistency checking and bookkeeping, VLP also supports executable specifications, which provide a prototype of the desired application. After reviewing the principles of VLP, the paper outlines the structure of the ECASET environment in which VLP is embedded. In particular, it shows how the environment supports the stepwise derivation of specifications, from informal to formal, and how it supports specification‐in‐the‐large.

Software processes are long-lived entities. Careful design and thorough validation of software process models are necessary to ensure the quality of the process. They do not prevent, however, process models from undergoing change. Change requests may occur in the context of reuse, i.e. statically, in order to support software process model customization. They can also occur dynamically, while software process models are being executed, in order to support timely reaction as data are gathered from the field during process enactment. We discuss the mechanisms a process language should possess in order to support changes. We illustrate the solution adopted in the context of the SPADE environment and discuss how the proposed mechanisms can be used to model different policies for changing a software process model.>

Process modeling is an active research area. During the last few years, new languages and methods have been proposed to describe software processes. In this paper, the authors clarify the issues involved in software process modeling and identify the main approaches. They also review the main existing approaches and propose a classification scheme.>

TRIO is a formal notation for the logic-based specification of real-time systems. In this paper the language and its straightforward model-theoretic semantics are briefly summarized. Then the need for assigning a consistent meaning to TRIO specifications is discussed, with reference to a variety of underlying time structures such as infinite-time structures (both dense and discrete) and finite-time structures. The main motivation is the ability to validate formal specifications. A solution to this problem is presented, which gives a new, model-parametric semantics to the language. An algorithm for constructively verifying the satisfiability of formulas in the decidable cases is defined, and several important temporal properties of specifications are characterized.

A technique and an environment-supporting specialization of generalized software components are described. The technique is based on symbolic execution. It allows one to transform a generalized software component into a more specific and more efficient component. Specialization is proposed as a technique that improves software reuse. The idea is that a library of generalized components exists and the environment supports a designer in customizing a generalized component when the need arises for reusing it under more restricted conditions. It is also justified as a reengineering technique that helps optimize a program during maintenance. Specialization is supported by an interactive environment that provides several transformation tools: a symbolic executor/simplifier, an optimizer, and a loop refolder. The conceptual basis for these transformation techniques is described, examples of their application are given, and how they cooperate in a prototype environment for the Ada programming language is outlined.>

The authors introduce a high-level Petri net formalism-environment/relationship (ER) nets-which can be used to specify control, function, and timing issues. In particular, they discuss how time can be modeled via ER nets by providing a suitable axiomatization. They use ER nets to define a time notation that is shown to generalize most time Petri-net-based formalisms which appeared in the literature. They discuss how ER nets can be used in a specification support environment for a time-critical system and, in particular, the kind of analysis supported.>

Some basic semantic issues of a language for a reliable and provably correct real-time programs are discussed. The language is based on E.W. Dijkstra's guarded commands and on a proposal by V.H. Haase (1981). Haase's proposal is assessed, its semantic consistencies are shown, and corrections are proposed that give a sound basis for a real-time language based on guarded commands.>

The concept of incremental parsing is briefly introduced and motivated.A general shift-reduce incremental parser is presented and compared with the corresponding conventional parser in terms of speed of analysis and storage requirements.It is then shown that additional speed-up can be obtained in the particular case of LR parsing.It is suggested that the approach can be applied to other parsing algorithms and generalized to the whole compiling or interpreting process.

Abstract A system for assisting in the testing phase of compilers is described. The definition of the language to be compiled drives an automatic sentence generator. The language is described by an extended BNF grammar which can be augmented by actions to ensure contextual congruence, e.g. between definition and use of identifiers. For deep control of the structure of the produced sample the grammar can be described by step‐wise refinements: the generator is iteratively applied to each level of refinement, producing at last compilable, complete programs. The implementation is described and some experimental results are reported concerning PLZ, MINIPL and some other languages.

Separate compilation is a useful tool in the development, debugging, testing, and integration of modular systems.

An incremental parser is a device which is able to perform syntax analysis in an incremental way, avoiding complete reparsing of a program after each modification. The incremental parser presented extends the conventional LR parsing algorithm and its performance is compared with that of a conventional parser. Suggestions for an implementation and possible extensions to other parsing methods are also discussed.