Generation of thorough test oracles is an open problem. Popular test case generators, like EvoSuite and Randoop, rely on implicit, rule-based, and regression oracles that miss failures that depend on the semantics of the program under test. Formal specifications can yield test oracles but are expensive to create.Large Language Models (LLMs) have the potential to overcome these limitations. The few studies of using LLMs to generate test oracles use modest-sized public benchmarks, such as Defects4J, that are likely to be included in the LLM training data, which threatens the validity of the results.This paper presents an empirical study of the effectiveness of LLMs in generating test oracles. Our experiments use 13,866 test oracles, from 135 Java projects, that were created after the LLMs training cut-off dates. Thus, our dataset is unbiased.In our experiments, LLMs generated oracles with average mutation score of 43%—similar to the 45% score of human-designed test oracles. Our results also indicate that the test prefix and the methods called in the program under test provide sufficient information to generate good oracles, while additional code context does not bring relevant benefits. These findings provide actionable insights into using LLMs for automatic testing and highlight their current limitations in generating complex oracles.

The landscape of software engineering is undergoing a transformative shift driven by advancements in machine learning, Artificial Intelligence (AI), and autonomous systems. This roadmap article explores how these technologies are reshaping the field, positioning humans not only as end users but also as critical components within expansive software ecosystems. We examine the challenges and opportunities arising from this human-centered paradigm, including ethical considerations, fairness, and the intricate interplay between technical and human factors. By recognizing humans at the heart of the software lifecycle—spanning professional engineers, end users, and end user developers—we emphasize the importance of inclusivity, human-aligned workflows, and the seamless integration of AI-augmented socio-technical systems. As software systems evolve to become more intelligent and human-centric, software engineering practices must adapt to this new reality. This article provides a comprehensive examination of this transformation, outlining current trends, key challenges, and opportunities that define the emerging research and practice landscape, and envisioning a future where software engineering and AI work synergistically to place humans at the core of the ecosystem.

Artificial intelligence and recent advances in deep learning architectures, including transformer networks and large language models, change the way people think and act to solve problems. Software engineering, as an increasingly complex process to design, develop, test, deploy, and maintain large-scale software systems for solving real-world challenges, is profoundly affected by many revolutionary artificial intelligence tools in general and machine learning in particular. In this roadmap for artificial intelligence in software engineering, we highlight the recent deep impact of artificial intelligence on software engineering by discussing successful stories of applications of artificial intelligence to classic and new software development challenges. We identify the new challenges that the software engineering community has to address in the coming years to successfully apply artificial intelligence in software engineering, and we share our research roadmap toward the effective use of artificial intelligence in the software engineering profession, while still protecting fundamental human values. We spotlight three main areas that challenge the research in software engineering: the use of generative artificial intelligence and large language models for engineering large software systems, the need of large and unbiased datasets and benchmarks for training and evaluating deep learning and large language models for software engineering, and the need of a new code of digital ethics to apply artificial intelligence in software engineering.

The landscape of software engineering has dramatically changed in recent years. The impressive advances of artificial intelligence are just the latest and most disruptive innovation that has remarkably changed the software engineering research and practice. This special issue shares a roadmap to guide the software engineering community in this confused era. This roadmap is the outcome of a 2-day intensive discussion at the 2030 Software Engineering workshop. The roadmap spotlights and discusses seven main landmarks in the new software engineering landscape: artificial intelligence for software engineering, human aspects of software engineering, software security, verification and validation, sustainable software engineering, automatic programming, and quantum software engineering. This editorial summarizes the core aspects discussed in the 37 papers that comprise the seven sections of the special issue and guides the interested readers throughout the issue. This roadmap is a living body that we will refine with follow-up workshops that will update the roadmap for a series of forthcoming ACM TOSEM special issues.

Reusing test cases across apps that share similar functionalities reduces both the effort required to produce useful test cases and the time to offer reliable apps to the market. The main approaches to reuse test cases across apps combine different semantic matching and test generation algorithms to migrate test cases across Android apps. In this paper we define a general framework to evaluate the impact and effectiveness of different choices of semantic matching with Test Reuse approaches on migrating test cases across Android apps. We offer a thorough comparative evaluation of the many possible choices for the components of test migration processes. We propose an approach that combines the most effective choices for each component of the test migration process to obtain an effective approach. We report the results of an experimental evaluation on 8,099 GUI events from 337 test configurations. The results attest the prominent impact of semantic matching on test reuse. They indicate that sentence level perform better than word level embedding techniques. They surprisingly suggest a negligible impact of the corpus of documents used for building the word embedding model for the Semantic Matching Algorithm. They provide evidence that semantic matching of events of selected types perform better than semantic matching of events of all types. They show that the effectiveness of overall Test Reuse approach depends on the characteristics of the test suites and apps. The replication package that we make publicly available online (https://star.inf.usi.ch/#/software-data/11) allows researchers and practitioners to refine the results with additional experiments and evaluate other choices for test reuse components.

Toward the Future with Eight Issues Per YearI am pleased to make several announcements with this issue of ACM Transactions on Software Engineering and Methodology (TOSEM), including the publication of eight issues per year, the implementation of the human-centric software engineering continuous special section, the forthcoming 2030 Roadmap for software engineering special issue, and the introduction of a "new frontiers" track.The landscape of software engineering is dramatically changing: New technologies challenge software engineering with new problems and solutions, and software engineering grows and diversifies.The research on applications of artificial intelligence (AI) to software engineering is a hot topic.The articles in the TOSEM continuous special section on AI and software engineering now represent almost one-fifth of the accepted articles, while they were a tiny fraction only 5 years ago.Original submissions to ACM TOSEM more than tripled in the past 5 years, with a relevant geographic shift from a dominant role of Europe and North America, with 84% of accepted articles 5 years ago, to a balanced distribution and the excellent presence of Asia and Australia, with 50% of accepted articles from the Asia-Pacific region in the past 12 months.ACM TOSEM has addressed the new challenges with new initiatives and a timely evolution.We introduced the fast track, continuous special sections, RCR reports, and registered articles.The fast-impact track offers a timebound review turnaround time, with over 50% of the overall submissions reviewed within 60 days and 80% reviewed within 90 days.The continuous special sections on AI and software engineering and on security and software engineering offer teams of expert editors to thoroughly review articles in fast-growing areas of software engineering.The fast track and the continuous special sections host articles that present completely new research results, and they now represent 60% of articles published in TOSEM.The RCR report offers a stable forum to share artifacts, tools, and data in the long term.The registered reports provide early feedback on new ideas that require expensive experimental validation and motivate investing in long-term expensive experiments.In 2024 we will move on with eight issues per year, a new human-centric software engineering continuous special section, a new technical communication track, and a 2030 Roadmap for a software engineering special issue.ACM TOSEM has published four issues per year in the first 30 years of its existence (from 1992 to 2022), it has published six issues in 2023, and it will regularly publish eight issues per year starting in 2024.The publication of eight issues per year will dramatically reduce the time to publication, thus giving the early visibility that high-quality articles deserve in a fast-changing landscape.The new continuous special section on human-centric software engineering offers an expert board to review contributions in the extremely relevant and fast-emerging field of human factors

ICSE and the Incredible Contradictions of Software EngineeringOnce upon a time, we submitted our papers to the International Conference on Software Engineering (ICSE) at the end of August and presented them in May, and the community was debating about the long 7-month delay between the submission and presentation of new ideas in a fast-changing discipline such as software engineering.Today, we submit our papers to ICSE in March and present the new ideas in April... oops... in April 13 months later!In 2024, we meet at ICSE in April to discuss papers that we submitted in March 2023, letting the new ideas of the papers already submitted in March 2024 age for 11 more months up to the presentations at ICSE in April 2025.At the same time, we discuss the incredible acceleration of ideas, technology, and society.Software is the core component of the current technological revolution: AI is software, machine learning is software, virtual reality is software, the internet of things is software, the whole environment is, by and large, software.Software engineering is a key discipline in this fast-evolving time, and it has the main responsibility of shaping the leading edge of the current technology revolution.There is an obvious and alarming gap between the fast-evolving time of the technological revolution and the fast-growing delay of sharing new ideas and results.The main software engineering conferences have done an amazing job to improve the quality and consistency of the review process and offer excellent programs while handling a number of submissions that exploded in the past decade.The two submission cycles both distribute the huge review workload over a long period and improve the reviewers-authors interactions, thus enhancing fairness and consistency.Unfortunately, the timeframe between the first submission and the presentation of a paper dilates beyond the interval frame between two consecutive conference editions, leading to the paradox of presenting ideas and results 13 months after the initial submission, while technology changes on a monthly basis.A decade ago, the main software engineering journals were suffering a crisis of submissions.Back in 2014, ACM Transactions on Software Engineering and Methodology (TOSEM) received as few as 146 original submissions, one-third of the 496 submissions to the ICSE 2014 technical track.None of the software engineering journals was in the first Scientific Journal Rankings (SJR) quartile in 2017.The main software engineering conferences and journals worked together to counteract the decline of journals, and they introduced the Journal First practice that reverted the trend and brought healthy growth back to software engineering journals that has been beneficial for both journals and conferences.In 2023, ACM TOSEM received 495 original submissions, about 65% of the 780 submissions to the ICSE 2014 technical track, and the trend in 2024 is still positive.The three major software engineering journals are now back in the first SJR quartile for the "software" category, despite maintaining stable review turnaround times and acceptance rates over the years.

Announcing Six TOSEM Issues Per YearI am pleased to be able to make several announcements with this issue of ACM Transactions on Software Engineering and Methodology (TOSEM) , including the publication of six issues per year, the addition of new Associate Editors, and the implementation of Registered Papers and Replicated Computational Results (RCR) Reports.It is a pleasure to share the decision of moving from four to six issues per year.TOSEM has published four issues per year since the beginning in 1992 and has hosted few tens of papers per year till recently.The openings of the fast-impact paper track, continuous special sections, and survey papers has led to a healthy growth of both submissions and papers.The four issues of 2022 host a record number of 85 papers, with a constant growth from the 17 papers published in the four issues of 2017, the bottom number of publications in the 30-years history of TOSEM.The healthy growth of publications per issue cannot prevent the growth of the backlog of accepted papers and the consequent time to publication.Six issues per year allows TOSEM to keep a small publication backlog and timely publish new and exciting results as soon as the papers are accepted.

This paper presents Prevent, a fully unsupervised approach to predict and localize failures in distributed enterprise applications.Software failures in production are unavoidable. Predicting failures and locating failing components online are the first steps to proactively manage faults in production. Many techniques predict failures from anomalous combinations of system metrics with supervised, weakly supervised, and semi-supervised learning models. Supervised approaches require large sets of labelled data not commonly available in large enterprise pplications, and address failure types that can be either captured with predefined rules or observed while training supervised odels.Preventintegrates the core ingredients of unsupervised approaches into a novel fully unsupervised approach to predict failures and localize failing resources. The results of experimenting with Preventon a commercially-compliant distributed cloud system indicate that Preventprovides more stable, reliable and timely predictions than supervised learning approaches, without requiring the often impractical training with labeled data.

Software systems may fail in production environments, causing system crashes, erroneous outputs, and overall system instability. Thoroughly testing software systems in development environments can reduce but not avoid failures, due to both the complexity of software applications, which may lead to a myriad of execution conditions impossible to sample exhaustively, and the many behaviors that emerge in production, which can be hardly predicted and exercised during development. This paper presents field-ready test cases, tests designed to run in production environments, aiming to proactively execute soft-ware components in yet unexplored execution scenarios, exposing error states before they result in system failures. Intuitively, the approach conceives the production environment as a testbed for opportunistically executing unit test cases that exploit the objects that become available as test data. The paper presents the results of a set of experiments with field-ready test cases that we produced for the JFreeChart and Apache Commons Lang libraries. Our field-ready test suites execute 64% of the faults that the original test suites miss, and exposes 33% of the missed faults.

Reusing test cases across similar applications can significantly reduce testing effort. Some recent test reuse approaches successfully exploit word embedding models to semantically match GUI events across Android apps. It is a common understanding that word embedding models trained on domain-specific corpora perform better on specialized tasks. Our recent study confirms this understanding in the context of Android test reuse. It shows that word embedding models trained with a corpus of the English descriptions of apps in the Google Play Store lead to a better semantic matching of Android GUI events. Motivated by this result, we hypothesize that we can further increase the effectiveness of semantic matching by partitioning the corpus of app descriptions into domain-specific corpora. Our experiments do not confirm our hypothesis. This paper sheds light on this unexpected negative result that contradicts the common understanding.

A class may need to obey temporal constraints in order to function correctly. For example, the correct usage protocol for an iterator is to always check whether there is a next element before asking for it; iterating over a collection when there are no items left leads to a NoSuchElementException. Automatic test case generation tools such as Randoop and EvoSuite do not have any notion of these temporal constraints. Generating test cases by randomly invoking methods on a new instance of the class under test may raise run time exceptions that do not necessarily expose software faults, but are rather a consequence of violations of temporal properties.

In this tutorial, we see how natural language processing and machine learning can help us address the open challenges of software testing. We overview the open challenges of testing autonomous and self-adaptive software systems, discuss the leading-edge technologies that can address the core issues, and see the latest progresses and future prospective of natural language processing and machine learning to cope with core problems.

No abstract available.

Automatic generators of GUI tests often fail to generate semantically relevant test cases, and thus miss important test scenarios. To address this issue, test adaptation techniques can be used to automatically generate semantically meaningful GUI tests from test cases of applications with similar functionalities.In this paper, we present ADAPTDROID, a technique that approaches the test adaptation problem as a search-problem, and uses evolutionary testing to adapt GUI tests (including oracles) across similar Android apps. In our evaluation with 32 popular Android apps, ADAPTDROID successfully adapted semantically relevant test cases in 11 out of 20 cross-app adaptation scenarios.

GUI testing is an important but expensive activity. Recently, research on test reuse approaches for Android applications produced interesting results. Test reuse approaches automatically migrate human-designed GUI tests from a source app to a target app that shares similar functionalities. They achieve this by exploiting semantic similarity among textual information of GUI widgets. Semantic matching of GUI events plays a crucial role in these approaches. In this paper, we present the first empirical study on semantic matching of GUI events. Our study involves 253 configurations of the semantic matching, 337 unique queries, and 8,099 distinct GUI events. We report several key findings that indicate how to improve semantic matching of test reuse approaches, propose SemFinder a novel semantic matching algorithm that outperforms existing solutions, and identify several interesting research directions.

Software is a core component of smart ecosystems, large ’system communities’ that emerge from the composition of autonomous, independent, and highly heterogeneous systems, like smart cities, smart grids, smart buildings. The systems that comprise smart ecosystems are not centrally owned, and mutually interact both explicitly and implicitly, leading to unavoidable contradictions and failures. The distinctive characteristics of smart ecosystems challenge software engineers with problems never addressed so far. In this paper we discuss the big challenge of defining a new concept of ’dependability’ and new approaches to reveal smart ecosystem failures.

Software testing depends on effective oracles. Implicit oracles, such as checks for program crashes, are widely applicable but narrow in scope. Oracles based on formal specifications can reveal application-specific failures, but specifications are expensive to obtain and maintain. Metamorphic oracles are somewhere in-between. They test equivalence among different procedures to detect semantic failures. Until now, the identification of metamorphic relations has been a manual and expensive process, except for few specific domains where automation is possible. We present MeMo, a technique and a tool to automatically derive metamorphic equivalence relations from natural language documentation, and we use such metamorphic relations as oracles in automatically generated test cases. Our experimental evaluation demonstrates that 1) MeMo can effectively and precisely infer equivalence metamorphic relations, 2) MeMo complements existing state-of-the-art techniques that are based on dynamic program analysis, and 3) metamorphic relations discovered with MeMo effectively detect defects when used as test oracles in automatically-generated or manually-written test cases.

Summary Concurrency testing is an important activity to expose concurrency faults in thread‐safe classes. A concurrent test for a thread‐safe class is a set of method call sequences that exercise the public interface of the class from multiple threads. Automatically generating fault‐revealing concurrent tests within an affordable time budget is difficult due to the huge search space of possible concurrent tests. In this paper, we present DepCon+, a novel approach that reduces the search space of concurrent tests by leveraging statically computed dependencies among public methods. DepCon+ exploits the intuition that concurrent tests can expose thread‐safety violations that manifest exceptions or deadlocks, only if they exercise some specific method dependencies. DepCon+ provides an efficient way to identify such dependencies by statically analysing the code and relies on the computed dependencies to steer the test generation towards those concurrent tests that exhibit the computed dependencies. We developed a prototype DepCon+ implementation for Java and evaluated the approach on 19 known concurrency faults of thread‐safe classes that lead to thread‐safety violations of either exception or deadlock type. The results presented in this paper show that DepCon+ is more effective than state‐of‐the‐art approaches in exposing the concurrency faults. The search space pruning of DepCon+ dramatically reduces the search space of possible concurrent tests, without missing any thread‐safety violations.

No abstract available.

In this paper we propose an approach for reusing formula solutions to reduce the impact of Satisfiability Modulo Theories (SMT) solvers on the scalability of symbolic program analysis. SMT solvers can efficiently handle huge expressions in relevant logic theories, but they still represent a main bottleneck to the scalability of symbolic analyses, like symbolic execution and symbolic model checking. Reusing proofs of formulas solved during former analysis sessions can reduce the amount of invocations of SMT solvers, thus mitigating the impact of SMT solvers on symbolic program analysis. Early approaches to reuse formula solutions exploit equivalence and inclusion relations among structurally similar formulas, and are strongly tighten to the specific target logics. In this paper, we present an original approach that reuses both satisfiability and unsatisfiability proofs shared among many formulas beyond only equivalent or related-by-implication formulas. Our approach straightforwardly generalises across multiple logics. It is based on the original concept of distance between formulas, which heuristically approximates the likelihood of formulas to share either satisfiability or unsatisfiability proofs. We show the efficiency and the generalisability of our approach, by instantiating the underlying distance function for formulas that belong to most popular logic theories handled by current SMT solvers, and confirm the effectiveness of the approach, by reporting experimental results on over nine millions formulas from five logic theories.

Comprehending the degree to which software components support testing is important to accurately schedule testing activities, train developers, and plan effective refactoring actions. Software testability estimates such property by relating code characteristics to the test effort. The main studies of testability reported in the literature investigate the relation between class metrics and test effort in terms of the size and complexity of the associated test suites. They report a moderate correlation of some class metrics to test-effort metrics, but suffer from two main limitations: (i) the results hardly generalize due to the small empirical evidence (datasets with no more than eight software projects); and (ii) mostly ignore the quality of the tests. However, considering the quality of the tests is important. Indeed, a class may have a low test effort because the associated tests are of poor quality, and not because the class is easier to test. In this paper, we propose an approach to measure testability that normalizes the test effort with respect to the test quality, which we quantify in terms of code coverage and mutation score. We present the results of a set of experiments on a dataset of 9,861 Java classes, belonging to 1,186 open source projects, with around 1.5 million of lines of code overall. The results confirm that normalizing the test effort with respect to the test quality largely improves the correlation between class metrics and the test effort. Better correlations result in better prediction power and thus better prediction of the test effort.

Assertion oracles are executable boolean expressions placed inside the program that should pass (return true) for all correct executions and fail (return false) for all incorrect executions. Because designing perfect assertion oracles is difficult, assertions often fail to distinguish between correct and incorrect executions. In other words, they are prone to false positives and false negatives. In this paper, we propose GAssert (Genetic ASSERTion improvement), the first technique to automatically improve assertion oracles. Given an assertion oracle and evidence of false positives and false negatives, GAssert implements a novel co-evolutionary algorithm that explores the space of possible assertions to identify one with fewer false positives and false negatives. Our empirical evaluation on 34 Java methods from 7 different Java code bases shows that GAssert effectively improves assertion oracles. GAssert outperforms two baselines (random and invariant-based oracle improvement), and is comparable with and in some cases even outperformed human-improved assertions.

No abstract available.

No abstract available.

Failures are unavoidable in complex software systems, and the intrinsic characteristics of cloud systems amplify the problem. Predicting failures before their occurrence by detecting anomalies in system metrics is a viable solution to enable failure preventing or mitigating actions. The most promising approaches for predicting failures exploit statistical analysis or machine learning to reveal anomalies and their correlation with possible failures. Statistical analysis approaches result in far too many false positives, which severely hinder their practical applicability, while accurate machine learning approaches need extensive training with seeded faults, which is often impossible in operative cloud systems. In this paper, we propose EmBeD, Energy-Based anomaly Detection in the cloud, an approach to detect anomalies at runtime based on the free energy of a Restricted Boltzmann Machine (RBM) model. The free energy is a stochastic function that can be used to efficiently score anomalies for detecting outliers. EmBeD analyzes the system behavior from raw metric data, does not require extensive training with seeded faults, and classifies the relation of anomalous behaviors with future failures with very few false positives. The experimental results presented in this paper confirm that EmBeD can precisely predict failure-prone behavior without training with seeded faults, thus overcoming the main limitations of current approaches.

Thread-safe classes are common in concurrent object-oriented programs. Testing such classes is important to ensure the reliability of the concurrent programs that rely on them. Recently, researchers have proposed the automated generation of concurrent (multi-threaded) tests to expose concurrency faults in thread-safe classes (thread-safety violations). However, generating fault-revealing concurrent tests within an affordable time-budget is difficult due to the huge search space of possible concurrent tests. In this paper, we present DepCon, an approach to effectively reduce the search space of concurrent tests by means of both parallel and conflict dependency analyses. DepCon is based on the intuition that only methods that can both interleave (parallel dependent) and access the same shared memory locations (conflict dependent) can lead to thread-safety violations when concurrently executed. DepCon implements an efficient static analysis to compute the parallel and conflict dependencies among the methods of a class and uses the computed dependencies to steer the generation of tests towards concurrent tests that exhibit the computed dependencies. We evaluated DepCon by experimenting with a prototype implementation for Java programs on a set of thread-safe classes with known concurrency faults. The experimental results show that DepCon is more effective in exposing concurrency faults than state-of-the-art techniques.

No abstract available.

No abstract available.

No abstract available.

No abstract available.

Testing software applications by interacting with their graphical user interface (GUI) is an expensive and complex process. Current automatic test case generation techniques implement explorative approaches that, although producing useful test cases, have a limited capability of covering semantically relevant interactions, thus frequently missing important testing scenarios. These techniques typically interact with the available widgets following the structure of the GUI, without any guess about the functions that are executed.

Procedure specifications are useful in many software development tasks. As one example, in automatic test case generation they can guide testing, act as test oracles able to reveal bugs, and identify illegal inputs. Whereas formal specifications are seldom available in practice, it is standard practice for developers to document their code with semi-structured comments. These comments express the procedure specification with a mix of predefined tags and natural language. This paper presents Jdoctor, an approach that combines pattern, lexical, and semantic matching to translate Javadoc comments into executable procedure specifications written as Java expressions. In an empirical evaluation, Jdoctor achieved precision of 92% and recall of 83% in translating Javadoc into procedure specifications. We also supplied the Jdoctor-derived specifications to an automated test case generation tool, Randoop. The specifications enabled Randoop to generate test cases of higher quality.

Developing correct and efficient concurrent programs is difficult and error-prone, due to the complexity of thread synchronization. Often, developers alleviate such problem by relying on thread-safe classes, which encapsulate most synchronization-related challenges. Thus, testing such classes is crucial to ensure the reliability of the concurrency aspects of programs. Some recent techniques and corresponding tools tackle the problem of testing thread-safe classes by automatically generating concurrent tests. In this paper, we present a comprehensive study of the state-of-the-art techniques and an independent empirical evaluation of the publicly available tools. We conducted the study by executing all tools on the JaConTeBe benchmark that contains 47 well-documented concurrency faults. Our results show that 8 out of 47 faults (17%) were detected by at least one tool. By studying the issues of the tools and the generated tests, we derive insights to guide future research on improving the effectiveness of automated concurrent test generation.

Many modern software systems are composed of multiple execution flows that run simultaneously, spanning from applications designed to exploit the power of modern multi-core architectures to distributed systems consisting of multiple components deployed on different physical nodes. We collectively refer to such systems as concurrent systems. Concurrent systems are difficult to test, since the faults that derive from their concurrent nature depend on the interleavings of the actions performed by the individual execution flows. Testing techniques that target these faults must take into account the concurrency aspects of the systems. The increasingly rapid spread of parallel and distributed architectures led to a deluge of concurrent software systems, and the explosion of testing techniques for such systems in the last decade. The current lack of a comprehensive classification, analysis and comparison of the many testing techniques for concurrent systems limits the understanding of the strengths and weaknesses of each approach and hampers the future advancements in the field. This survey provides a framework to capture the key features of the available techniques to test concurrent software systems, identifies a set of classification criteria to review and compare the available techniques, and discusses in details their strengths and weaknesses, leading to a thorough assessment of the field and paving the road for future progresses.

Many symbolic program analysis techniques rely on SMT solvers to verify properties of programs. Despite the remarkable progress made in the development of such tools, SMT solvers still represent a main bottleneck to the scalability of these techniques. Recent approaches tackle this bottleneck by reusing solutions of formulas that recur during program analysis, thus reducing the number of queries to SMT solvers. Current approaches only reuse solutions across formulas that are equivalent to, contained in or implied by other formulas, as identified through a set of predefined rules, and cannot reuse solutions across formulas that differ in their structure, even if they share some potentially reusable solutions. In this paper, we propose a novel approach that can reuse solutions across formulas that share at least one solution, regardless of their structural resemblance. Our approach exploits a novel heuristic to efficiently identify solutions computed for previously solved formulas and most likely shared by new formulas. The results of an empirical evaluation of our approach on two different logics show that our approach can identify on average more reuse opportunities and is markedly faster than competing approaches.

Field failures, that is, failures caused by faults that escape the testing phase leading to failures in the field, are unavoidable. Improving verification and validation activities before deployment can identify and timely remove many but not all faults, and users may still experience a number of annoying problems while using their software systems.This paper investigates the nature of field failures, to understand to what extent further improving in-house verification and validation activities can reduce the number of failures in the field, and frames the need of new approaches that operate in the field.We report the results of the analysis of the bug reports of five applications belonging to three different ecosystems, propose a taxonomy of field failures, and discuss the reasons why failures belonging to the identified classes cannot be detected at design time but shall be addressed at runtime. We observe that many faults (70%) are intrinsically hard to detect at design-time.

Despite the recent improvements in automatic test case generation, handling complex data structures as test inputs is still an open problem. Search-based approaches can generate sequences of method calls that instantiate structured inputs to exercise a relevant portion of the code, but fall short in building inputs to execute program elements whose reachability is determined by the structural features of the input structures themselves. Symbolic execution techniques can effectively handle structured inputs, but do not identify the sequences of method calls that instantiate the input structures through legal interfaces. In this paper, we propose a new approach to automatically generate test cases for programs with complex data structures as inputs. We use symbolic execution to generate path conditions that characterise the dependencies between the program paths and the input structures, and convert the path conditions to optimisation problems that we solve with search-based techniques to produce sequences of method calls that instantiate those inputs. Our preliminary results show that the approach is indeed effective in generating test cases for programs with complex data structures as inputs, thus opening a promising research direction.

Reproducing field failures is the first essential step for understanding, localizing and removing faults. Reproducing concurrency field failures is hard due to the need of synthesizing a test code jointly with a thread interleaving that induce the failure in the presence of limited information from the field. Current techniques for reproducing concurrency failures focus on identifying failure-inducing interleavings, leaving largely open the problem of synthesizing the test code that manifests such interleavings. In this paper, we present ConCrash, a technique to automatically generate test codes that reproduce concurrency failures that violate thread-safety from crash stacks, which commonly summarize the conditions of field failures. ConCrash efficiently explores the huge space of possible test codes to identify a failure-inducing one by using a suitable set of search pruning strategies. Combined with existing techniques for exploring interleavings, ConCrash automatically reproduces a given concurrency failure that violates the thread-safety of a class by identifying both a failure-inducing test code and corresponding interleaving. In the paper, we define the ConCrash approach, present a prototype implementation of ConCrash, and discuss the experimental results that we obtained on a known set of ten field failures that witness the effectiveness of the approach.

Inferring models of program behavior from execution samples can provide useful information about a system, also in the increasingly common case of systems that evolve and adapt in their lifetime, and without requiring large developers' effort. Techniques for learning models of program behavior from execution traces shall address conflicting challenges of recall, specificity and performance: They shall generate models that comprehensively represent the system behavior (recall) while limiting the amount of illegal behaviors that may be erroneously accepted by the model (specificity), and should infer the models within a reasonable time budget to process industrial scale systems (performance). In our early work, we designed GK-tail, an approach that can infer guarded finite state machines that model the behavior of object-oriented programs in terms of sequences of method calls and constraints on the parameter values. GK-tail addresses well two of the three main challenges, since it infers guarded finite state machines with a high level of recall and specificity, but presents severe limitations in terms of performance that reduce its scalability. In this paper, we present GK-tail+, a new approach to infer guarded finite state machines from execution traces of object-oriented programs. GK-tail+ proposes a new set of inference criteria that represent the core element of the inference process: It largely reduces the inference time of GK-tail while producing guarded finite state machines with a comparable level of recall and specificity. Thus, GK-tail+ advances the preliminary results of GK-tail by addressing all the three main challenges of learning models of program behavior from execution traces.

Test suites should test exceptional behavior to detect faults in error-handling code. However, manually-written test suites tend to neglect exceptional behavior. Automatically-generated test suites, on the other hand, lack test oracles that verify whether runtime exceptions are the expected behavior of the code under test.

We present the Java Bytecode Symbolic Executor (JBSE), a symbolic executor for Java programs that operates on complex heap inputs. JBSE implements both the novel Heap EXploration Logic (HEX), a symbolic execution approach to deal with heap inputs, and the main state-of-the-art approaches that handle data structure constraints expressed as either executable programs (repOk methods) or declarative specifications. JBSE is the first symbolic executor specifically designed to deal with programs that operate on complex heap inputs, to experiment with the main state-of-the-art approaches, and to combine different decision procedures to explore possible synergies among approaches for handling symbolic data structures.

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.

Cloud technology is rapidly substituting classic computing solutions, and challenges the community with new problems. In this paper we focus on controllers for cloud application elasticity, and propose a novel solution for self-adaptive cloud controllers based on Kriging models. Cloud controllers are application specific schedulers that allocate resources to applications running in the cloud, aiming to meet the quality of service requirements while optimizing the execution costs. General-purpose cloud resource schedulers provide sub-optimal solutions to the problem with respect to application-specific solutions that we call cloud controllers. In this paper we discuss a general way to design self-adaptive cloud controllers based on Kriging models. We present Kriging models, and show how they can be used for building efficient controllers thanks to their unique characteristics. We report experimental data that confirm the suitability of Kriging models to support efficient cloud control and open the way to the development of a new generation of cloud controllers.

Structural coverage metrics, and in particular branch coverage, are popular approaches to measure the thoroughness of test suites. Unfortunately, the presence of elements that are not executable in the program under test and the difficulty of generating test cases for rare conditions impact on the effectiveness of the coverage obtained with current approaches. In this paper, we propose a new approach that combines symbolic execution and symbolic reachability analysis to improve the effectiveness of branch testing. Our approach embraces the ideal definition of branch coverage as the percentage of executable branches traversed with the test suite, and proposes a new bidirectional symbolic analysis for both testing rare execution conditions and eliminating infeasible branches from the set of test objectives. The approach is centered on a model of the analyzed execution space. The model identifies the frontier between symbolic execution and symbolic reachability analysis, to guide the alternation and the progress of bidirectional analysis towards the coverage targets. The experimental results presented in the paper indicate that the proposed approach can both find test inputs that exercise rare execution conditions that are not identified with state-of-the-art approaches and eliminate many infeasible branches from the coverage measurement. It can thus produce a modified branch coverage metric that indicates the amount of feasible branches covered during testing, and helps team leaders and developers in estimating the amount of not-yet-covered feasible branches. The approach proposed in this paper suffers less than the other approaches from particular cases that may trap the analysis in unbounded loops.

Redundancy is the presence of different elements with the same functionality. In software, redundancy is useful (and used) in many ways, for example for fault tolerance and reliability engineering, and in self-adaptive and self-checking programs. However, despite the many uses, we still do not know how to measure software redundancy to support a proper and effective design. If, for instance, the goal is to improve reliability, one might want to measure the redundancy of a solution to then estimate the reliability gained with that solution. Or one might compare alternative solutions to choose the one that expresses more redundancy and therefore, presumably, more reliability. We first formalize a notion of redundancy whereby two code fragments are considered redundant when they achieve the same functionality with different executions. On the basis of this abstract and general notion, we then develop a concrete method to obtain a meaningful quantitative measure of software redundancy. The results we obtain are very positive: we show, through an extensive experimental analysis, that it is possible to distinguish code that is only minimally different, from truly redundant code, and that it is even possible to distinguish low-level code redundancy from high-level algorithmic redundancy. We also show that the measurement is significant and useful for the designer, as it can help predict the effectiveness of techniques that exploit redundancy.

Data flow testing has recently attracted new interest in the context of testing object oriented systems, since data flow information is well suited to capture relations among the object states, and can thus provide useful information for testing method interactions. Unfortunately, classic data flow testing, which is based on static analysis of the source code, fails to identify many important data flow relations due to the dynamic nature of object oriented systems. In this paper, we propose a new technique to generate test cases for object oriented software. The technique exploits useful inter-procedural data flow information extracted dynamically from execution traces for object oriented systems. The technique is designed to enhance an initial test suite with test cases that exercise complex state based method interactions. The experimental results indicate that dynamic data flow testing can indeed generate test cases that exercise relevant behaviors otherwise missed by both the original test suite and by test suites that satisfy classic data flow criteria.

Symbolic analysis techniques have largely improved over the years, and are now approaching an industrial maturity level. One of the main limitations to the scalability of symbolic analysis is the impact of constraint solving that is still a relevant bottleneck for the applicability of symbolic techniques, despite the dramatic improvements of the last decades. In this paper we discuss a novel approach to deal with the constraint solving bottleneck. Starting from the observation that constraints may recur during the analysis of the same as well as different programs, we investigate the advantages of complementing constraint solving with searching for the satisfiability proof of a constraint in a repository of constraint proofs. We extend recent proposals with powerful simplifications and an original canonical form of the constraints that reduce syntactically different albeit equivalent constraints to the same form, and thus facilitate the search for equivalent constraints in large repositories. The experimental results we attained indicate that the proposed approach improves over both similar solutions and state of the art constraint solvers.

Symbolic analysis is a core component of many automatic test generation and program verication approaches. To verify complex software systems, test and analysis techniques shall deal with the many aspects of the target systems at different granularity levels. In particular, testing software programs that make extensive use of heap data structures at unit and integration levels requires generating suitable input data structures in the heap. This is a main challenge for symbolic testing and analysis techniques that work well when dealing with numeric inputs, but do not satisfactorily cope with heap data structures yet. In this paper we propose a language HEX to specify invariants of partially initialized data structures, and a decision procedure that supports the incremental evaluation of structural properties in HEX. Used in combination with the symbolic execution of heap manipulating programs, HEX prevents the exploration of invalid states, thus improving the eefficiency of program testing and analysis, and avoiding false alarms that negatively impact on verication activities. The experimental data conrm that HEX is an effective and efficient solution to the problem of testing and analyzing heap manipulating programs, and outperforms the alternative approaches that have been proposed so far.

Despite the best intentions, the competence, and the rigorous methods of designers and developers, software is often delivered and deployed with faults. To cope with imperfect software, researchers have proposed the concept of self-healing for software systems. The ambitious goal is to create software systems capable of detecting and responding “autonomically” to functional failures, or perhaps even preempting such failures, to maintain a correct functionality, possibly with acceptable degradation. We believe that self-healing can only be an expression of some form of redundancy, meaning that, to automatically fix a faulty behavior, the correct behavior must be already present somewhere, in some form, within the software system either explicitly or implicitly. One approach is to deliberately design and develop redundant systems, and in fact this kind of deliberate redundancy is the essential ingredient of many fault tolerance techniques. However, this type of redundancy is also generally expensive and does not always satisfy the time and cost constraints of many software projects. With this article we take a different approach. We observe that modern software systems naturally acquire another type of redundancy that is not introduced deliberately but rather arises intrinsically as a by-product of modern modular software design. We formulate this notion of intrinsic redundancy and we propose a technique to exploit it to achieve some level of self-healing. We first demonstrate that software systems are indeed intrinsically redundant. Then we develop a way to express and exploit this redundancy to tolerate faults with automatic workarounds. In essence, a workaround amounts to replacing some failing operations with alternative operations that are semantically equivalent in their intended effect, but that execute different code and ultimately avoid the failure. The technique we propose finds such workarounds automatically. We develop this technique in the context of Web applications. In particular, we implement this technique within a browser extension, which we then use in an evaluation with several known faults and failures of three popular Web libraries. The evaluation demonstrates that automatic workarounds are effective: out of the nearly 150 real faults we analyzed, 100 could be overcome with automatic workarounds, and half of these workarounds found automatically were not publicly known before.

editorial Free AccessIntroduction to the Special Issue on ISSTA 2013 Editors: Mark Harman University College London, UK University College London, UKView Profile , Mauro Pezzé University of Milano Bicocca and University of Lugano University of Milano Bicocca and University of LuganoView Profile Authors Info & Claims ACM Transactions on Software Engineering and MethodologyVolume 24Issue 4August 2015 Article No.: 21pp 1–3https://doi.org/10.1145/2809789Published:02 September 2015Publication History 0citation219DownloadsMetricsTotal Citations0Total Downloads219Last 12 Months10Last 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

Despite the recent advances in automatic test generation, testers must still write test oracles manually. If formal specifications are available, it might be possible to use decision procedures derived from those specifications. We present a technique that is based on a form of specification but also leverages more information from the system under test. We assume that the system under test is somewhat redundant, in the sense that some operations are designed to behave like others but their executions are different. Our experience in this and previous work indicates that this redundancy exists and is easily documented. We then generate oracles by cross-checking the execution of a test with the same test in which we replace some operations with redundant ones. We develop this notion of cross-checking oracles into a generic technique to automatically insert oracles into unit tests. An experimental evaluation shows that cross-checking oracles, used in combination with automatic test generation techniques, can be very effective in revealing faults, and that they can even improve good hand-written test suites.

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.

This paper investigates the limits of current data flow testing approaches from a radically novel viewpoint, and shows that the static data flow techniques used so far in data flow testing to identify the test objectives fail to represent the universe of data flow relations entailed by a program. This paper compares the data flow relations computed with static data flow approaches with the ones observed while executing the program. To this end, the paper introduces a dynamic data flow technique that collects the data flow relations observed during testing. The experimental data discussed in the paper suggest that data flow testing based on static techniques misses many data flow test objectives, and indicate that the amount of missing objectives (false negatives) can be more limiting than the amount of infeasible data flow relations identified statically (false positives). This opens a new area of research of (dynamic) data flow testing techniques that can better encompass the test objectives of data flow testing.

Applications that process complex data, such as maps, personal data, book information, travel data, etc., are becoming extremely common. Testing such applications is hard, because they require realistic and coherent test inputs that are expensive to generate manually and difficult to synthesize automatically. So far the research on test case generation techniques has focused mostly on generating test sequences and synthetic test inputs, and has payed little attention to the generation of complex test inputs.

Software components are usually redundant, since their interface offers different operations that are equivalent in their functional behavior. Several reliability techniques exploit this redundancy to either detect or tolerate faults in software. Metamorphic testing, for instance, executes pairs of sequences of operations that are expected to produce equivalent results, and identifies faults in case of mismatching outcomes. Some popular fault tolerance and self-healing techniques execute redundant operations in an attempt to avoid failures at runtime. The common assumption of these techniques, though, is that such redundancy is known a priori. This means that the set of operations that are supposed to be equivalent in a given component should be available in the specifications. Unfortunately, inferring this information manually can be expensive and error prone. This paper proposes a search-based technique to synthesize sequences of method invocations that are equivalent to a target method within a finite set of execution scenarios. The experimental results obtained on 47 methods from 7 classes show that the proposed approach correctly identifies equivalent method sequences in the majority of the cases where redundancy was known to exist, with very few false positives.

SUMMARY Testing GUI‐based applications is hard and time consuming because it requires exploring a potentially huge execution space by interacting with the graphical interface of the applications. Manual testing can cover only a small subset of the functionality provided by applications with complex interfaces, and thus, automatic techniques are necessary to extensively validate GUI‐based systems. This paper presents AutoBlackTest, a technique to automatically generate test cases at the system level. AutoBlackTest uses reinforcement learning, in particular Q‐learning, to learn how to interact with the application under test and stimulate its functionalities. When used to complement the activity of test designers, AutoBlackTest reuses the information in the available test suites to increase its effectiveness. The empirical results show that AutoBlackTest can sample better than state of the art techniques the behaviour of the application under test and can reveal previously unknown problems by working at the system level and interacting only through the graphical user interface. Copyright © 2014 John Wiley & Sons, Ltd.

SUMMARY Software systems evolve incrementally both during and after development, and many test cases become obsolete while software evolves. Updating test suites in the context of software evolution is a complex and time consuming activity. This article focuses on the problem of updating test suites automatically, and identifies eight scenarios that allow either to repair test cases or to use test cases to generate new ones, and proposes eight test evolution algorithms that automatically repair and generate test cases by adapting existing ones. This article presents a framework, TestCareAssistant (TCA), that implements the algorithms to support the evolution of test suites written in Java. The framework has been extensively evaluated on five different open source projects where it has been applied to repair 138 broken test cases, and to generate the test cases for 727 new classes and 2462 new methods. The results obtained with TCA indicate that the approach can successfully repair 90% of the broken test cases, create test cases that cover a large amount of code and complement the test cases that can be generated by state of the art techniques. Copyright © 2014 John Wiley & Sons, Ltd.

No abstract available.

We present a technique to make applications resilient to failures. This technique is intended to maintain a faulty application functional in the field while the developers work on permanent and radical fixes. We target field failures in applications built on reusable components. In particular, the technique exploits the intrinsic redundancy of those components by identifying workarounds consisting of alternative uses of the faulty components that avoid the failure. The technique is currently implemented for Java applications but makes little or no assumptions about the nature of the application, and works without interrupting the execution flow of the application and without restarting its components. We demonstrate and evaluate this technique on four mid-size applications and two popular libraries of reusable components affected by real and seeded faults. In these cases the technique is effective, maintaining the application fully functional with between 19% and 48% of the failure-causing faults, depending on the application. The experiments also show that the technique incurs an acceptable runtime overhead in all cases.

Unit testing aims to ensure that methods correctly implement the specified and implied pre- and post-conditions, while integration testing ensures that modules correctly follow interaction protocols. While the generation of unit test cases has been explored extensively in the literature, there is still little work on the generation of integration test cases. In this paper we present a new technique to generate integration test cases that leverages existing unit test cases. Our key observation is that both, unit and integration testing, use method calls as the atoms to construct test cases from. Unit tests contain information on how to instantiate classes in meaningful ways, how to construct arguments for method calls, and what the resulting system state should be after calling methods with those arguments. We use this information to construct more complex test cases that focus on class interactions rather than on individual state transformations caused by single method calls. This paper presents the approach and shows that the generated test cases can find interesting faults, compared to test suites generated with state of the art approaches.

Symbolic execution suffers from problems when analyzing programs that handle complex data structures as their inputs and take decisions over non-linear expressions. For these programs, symbolic execution may incur invalid inputs or unidentified infeasible traces, and may raise large amounts of false alarms. Some symbolic executors tackle these problems by introducing executable preconditions to exclude invalid inputs, and some solvers exploit rewrite rules to address non linear problems. In this paper, we discuss the core limitations of executable preconditions, and address these limitations by proposing invariants specifically designed to harmonize with the lazy initialization algorithm. We exploit rewrite rules applied within the symbolic executor, to address simplifications of inverse relationships fostered from either program-specific calculations or the logic of the verification tasks. We present a symbolic executor that integrates the two techniques, and validate our approach against the verification of a relevant set of properties of the Tactical Separation Assisted Flight Environment. The empirical data show that the integrated approach can improve the effectiveness of symbolic execution.

To design effective exception handlers, developers must predict at design time the exceptional events that may occur at runtime, and must implement the corresponding handlers on the basis of their predictions. Designing exception handlers for component-based software systems is particularly difficult because the information required to build handlers is distributed between component and application developers. Component developers know the internal details of the components but ignore the applications, while application developers own the applications but cannot access the details required to implement handlers in components. This article addresses the problem of automatically healing the infield failures that are caused by faulty integration of OTS components. In the article, we propose a technique and a methodology to decouple the tasks of component and application developers, who will be able to share information asynchronously and independently, and communicate implicitly by developing and deploying what we call healing connectors. Component developers implement healing connectors on the basis of information about the integration problems frequently experienced by application developers. Application developers easily and safely install healing connectors in their applications without knowing the internal details of the connectors. Healing connectors heal failures activated by exceptions raised in the OTS components actually deployed in the system. The article defines healing connectors, introduces a methodology to develop and deploy healing connectors, and presents several case studies that indicate that healing connectors are effective, reusable and efficient.

Service-oriented applications do not fully benefit from standard APIs yet, and many applications fail to use interchangeably all the services that implement a standard service API. This article presents an approach to develop adaptation strategies that improve service interchangeability for service-oriented applications based on standard APIs. In our approach, an adaptation strategy consists of sets of parametric adaptation plans (called test-and-adapt plans), which execute test cases to reveal the occurrence of interchangeability problems, and activate runtime adaptors according to the test results. Throughout this article, we formalize the structure of the parametric test-and-adapt plans and of their execution semantics, present an algorithm for identifying correct execution orders through sets of test-and-adapt plans, provide empirical evidence of the occurrence of interchangeability problems for sample applications and services, and discuss the effectiveness of the approach in terms of avoided failures, runtime overheads and development costs.

Summary form only given. Software is the cornerstone of the modern society. Many human activities rely on software systems that shall operate seamlessly 24/7, and failures in such systems may cause severe problems and considerable economic loss. To efficiently address a growing variety of increasingly complex activities, software systems rely on sophisticated technologies. Most software systems are assembled from modules and subsystems that are often developed by third party organization, and sometime are not even available at the system build time. This is the case for example of many Web applications that link Web services built and changed independently by third party organizations while the Web applications are running. The progresses of software engineering in the last decades have increased the productivity, reduced the costs and improved the reliability of software products, but have not eliminated the occurrence of field failures. Detecting and removing all faults before deployment is practically too expensive even for systems that are simple and fully available at design time, and impossible when systems are large and complex, and are dynamically linked to modules that may be developed and distributed only after the deployment of the system. The classic stop-and-go maintenance approaches that locate and fix field faults offline before deploying new system versions are important, but not sufficient to guarantee a seamless 24/7 behavior, because the faulty systems remain in operation until the faults have been removed and new systems redeployed [1]. On the other hand, classic fault tolerant approaches that constrain developers' freedom and rely on expensive mechanisms to avoid or mask faults do not match the cost requirements of many modern systems, and do not extend beyond the set of safety critical systems [2]. Self-healing systems and autonomic computing tackle these new challenges by moving activities from design to runtime. In self-healing systems, the borderline between design and runtime activities fades, and both design and maintenance activities must change to enable activities such as fault diagnoses and fixes to be performed fully automatically and at runtime. Maintenance activities rely on information that are usually available at design time are are not part of the system runtime infrastructure. For example, corrective maintenance requires some knowledge about the expected system behavior to locate and fix the faults, while adaptive and perfective maintenance requires some knowledge about libraries and components to identify new modules that better cope with the the changes in the requirements and in the environment. In classic maintenance approaches, this knowledge is mastered by the developers, who gather and use the required information offline to deal with the emerging maintenance problems. In self healing systems the knowledge required for maintenance activities shall be available at runtime. Self healing systems shall be designed with enough embedded knowledge to deal with unplanned events, and shall be able to exploit this information automatically and at runtime to recover from unexpected situations, like field failures. The challenges of designing powerful self-healing systems relies in the ability to minimize the amount of extra knowledge to be provided at design time, while feeding a powerful automatic recovery mechanism. An interesting approach relies on the observation that software systems are redundant by nature, and exploits the intrinsic redundancy of software system to fix faults, thus minimizing the extra effort required at design time to feed the self-healing mechanism [3]. The intrinsic redundancy of software stems from design and reusability practice: the reuse of libraries may results in different ways to achieve the same or similar results, the design for modularity may produce methods with equivalent behavior, backward compatibility may keep deprecated and new implementations in the same system. For example, libraries like Ant and Log4J implement several functionalities already available in the standard Java libraries to improve efficiency or usability, while graphical libraries, like SWT, Swing and AWT, provide overlapping functionality that may be available in systems that include two or more of these libraries. This redundancy is available for free at runtime, and can be exploited both to design self-healing mechanisms that can be automatically activated to solve faulty situations at runtime, and to improve maintenance mechanisms by facilitating failure reproduction and fault localization and fixing.

Automatic test case generation is a key ingredient of an efficient and cost-effective software verification process. In this paper we focus on testing applications that interact with the users through a GUI, and present AutoBlackTest, a technique to automatically generate test cases at the system level. AutoBlackTest uses reinforcement learning, in particular Q-Learning, to learn how to interact with the application under test and stimulate its functionalities. The empirical results show that AutoBlackTest can execute a relevant portion of the code of the application under test, and can reveal previously unknown problems by working at the system level and interacting only through the GUI.

Software systems evolve during development and maintenance, and many test cases designed for the early versions of the system become obsolete during the software lifecycle. Repairing test cases that do not compile due to changes in the code under test and generating new test cases to test the changed code is an expensive and time consuming activity that could benefit from automated approaches. In this paper we propose an approach for automatically repairing and generating test cases during software evolution. Differently from existing approaches to test case generation, our approach uses information available in existing test cases, defines a set of heuristics to repair test cases invalidated by changes in the software, and generate new test cases for evolved software. The results obtained with a prototype implementation of the technique show that the approach can effectively maintain evolving test suites, and perform well compared to competing approaches.

In this paper we present AutoBlackTest, a tool for the automatic generation of test cases for interactive applications. AutoBlackTest interacts with the application though its GUI, and uses reinforcement learning techniques to understand the interaction modalities and to generate relevant testing scenarios. Early results show that the tool has the potential of automatically discovering bugs and generating useful system and regression test suites.

Many software components are provided with incomplete specifications and little access to the source code. Reusing such gray-box components can result in integration faults that can be difficult to diagnose and locate. In this paper, we present Behavior Capture and Test (BCT), a technique that uses dynamic analysis to automatically identify the causes of failures and locate the related faults. BCT augments dynamic analysis techniques with model-based monitoring. In this way, BCT identifies a structured set of interactions and data values that are likely related to failures (failure causes), and indicates the components and the operations that are likely responsible for failures (fault locations). BCT advances scientific knowledge in several ways. It combines classic dynamic analysis with incremental finite state generation techniques to produce dynamic models that capture complementary aspects of component interactions. It uses an effective technique to filter false positives to reduce the effort of the analysis of the produced data. It defines a strategy to extract information about likely causes of failures by automatically ranking and relating the detected anomalies so that developers can focus their attention on the faults. The effectiveness of BCT depends on the quality of the dynamic models extracted from the program. BCT is particularly effective when the test cases sample the execution space well. In this paper, we present a set of case studies that illustrate the adequacy of BCT to analyze both regression testing failures and rare field failures. The results show that BCT automatically filters out most of the false alarms and provides useful information to understand the causes of failures in 69 percent of the case studies.

Faults in Web APIs may escape the testing process, and therefore affect thousands of Web applications. As a consequence, users of these applications might suffer from related failures for a long time until proper fixes are released by the Web API developers. In this paper we present RAW, a tool that tries to find workarounds automatically and at runtime, thereby reducing the negative impact of faults in Web applications. Runtime and automatically deployed workarounds serve as a temporary relief for application users while proper fixes are developed and released.

The Software Engineering for Adaptive and Self-managing Systems (SEAMS) workshop has consolidated the interest in the software engineering community on self-adaptive and self-managing systems. SEAMS provides a forum for researchers and practitioners to share new results, discuss challenging issues, raise awareness, and promote collaboration within the community. The SEAMS 2010 workshop aims to continue the success of previous ICSE SEAMS workshops: in Shanghai in 2006, in Minneapolis in 2007, in Leipzig in 2008, and in Vancouver in 2009.

When software systems evolve, for example due to fault fixes, modification of functionalities or refactoring activities, test cases may become obsolete thus generating wrong results or even not being executable or compilable. Maintaining test cases is expensive and time consuming, and often test cases are discarded by software developers due to high maintenance costs. This paper presents TestCareAssistant, a technique that combines data-flow analysis with program diffing for automatically repairing test cases that become obsolete because of changes in method declarations (addition, removal, or type modification of parameters or return values). The paper illustrates the efficacy of TestCareAssistant by analyzing the impact of method declarations changes on the executability of test cases, and by presenting the preliminary results of applying TestCareAssistant to repair 22 test cases.

Modern Web applications are often hosted in a virtualized cloud computing infrastructure, and can dynamically scale in response to unpredictable changes in the workload to guarantee a given service level agreement. In this paper we propose to use Kriging surrogate models to approximate the performance profile of virtualized, multi-tier Web applications. The model is first built through a set of automated and controlled experiments at staging time, and can be later updated and refined by monitoring the Web application deployed in production. We claim that surrogate modeling makes a very good candidate for a model-driven approach to the engineering of an autonomic controller. Our experimental evaluation shows that the model predictions are faithful to the observed system's performance, they improve with an increasing amount of samples and they can be computed quickly. We also provide evidence that the model can be effectively used to synthetize an aggregated objective function, a critical component of the autonomic controller. The approach is evaluated in the context of a RESTful Web service composition case study deployed on the RESERVOIR cloud.

We present a technique that finds and executes workarounds for faulty Web applications automatically and at runtime. Automatic workarounds exploit the inherent redundancy of Web applications, whereby a functionality of the application can be obtained through different sequences of invocations of Web APIs. In general, runtime workarounds are applied in response to a failure, and require that the application re-main in a consistent state before and after the execution of a workaround. Therefore, they are ideally suited for inter-active Web applications, since those allow the user to act as a failure detector with minimal effort, and also either use read-only state or manage their state through a trans-actional data store. In this paper we focus on faults found in the access libraries of widely used Web applications such as Google Maps. We start by classifying a number of re-ported faults of the Google Maps and YouTube APIs that have known workarounds. From those we derive a number of general and API-specific program-rewriting rules, which we then apply to other faults for which no workaround is known. Our experiments show that workarounds can be readily de-ployed within Web applications, through a simple client-side plug-in, and that program-rewriting rules derived from ele-mentary properties of a common library can be effective in finding valid and previously unknown workarounds.

Developers frequently integrate complex COTS frameworks and components in software applications. COTS products are often only partially documented, and developers may misuse technologies and introduce integration faults, as witnessed by the many entries in fault repositories. Once identified, common integration problems and their fixes are usually documented in forums and fault repositories on the Web, but this does not prevent them to occur in the field when COTS products are reused.

Classic fault localization techniques can automatically provide information about the suspicious code blocks that are likely responsible for observed failures. This information is useful, but not sufficient to completely understand the causes of failing executions, which still require further (time-consuming) investigations to be exactly identified. A useful and comprehensive source of information is frequently given by the set of unexpected events that have been observed during failures. Sequences of unexpected events are usually simple to be interpret, and testers can guess the expected correct sequences of events from the faulty sequences. In this paper, we present a tool that automatically identifies anomalous events that likely caused failures, filters the possible false positives, and presents the resulting data by building views that show chains of cause-effect relations, i.e., views that show when anomalous events are caused by other anomalous events. The use of the technique to investigate a fault in the Tomcat application server is also presented in the paper.

Many modern software systems dynamically discover and integrate third party libraries, components and services that comply with standard APIs. Compliance with standard APIs facilitates dynamic binding, but does not always guarantee full behavioral compatibility. For instance, problems that derive from behavior incompatibility are quite frequent in service-oriented applications that dynamically bind service implementations that match API specifications.

Many testing and analysis techniques use finite state models to validate and verify the quality of software systems. Since the specification of such models is complex and time-consuming, researchers defined several techniques to extract finite state models from code and traces. Automatically generating models requires much less effort than designing them, and thus eases the verification and validation of large software systems. However, when models are inferred automatically, the precision of the mining process is critical. Behavioral models mined with imprecise processes can include many spurious behaviors, and can thus compromise the results of testing and analysis techniques that use those models.

Dynamic analysis of software systems produces behavioral models that are useful for analysis, verification and testing.

No abstract available.

Software engineers frequently update COTS components integrated in component-based systems, and can often chose among many candidates produced by different vendors. This paper tackles both the problem of quickly identifying components that are syntactically compatible with the interface specifications, but badly integrate in target systems, and the problem of automatically generating regression test suites. The technique proposed in this paper to automatically generate compatibility and prioritized test suites is based on behavioral models that represent component interactions, and are automatically generated while executing the original test suites on previous versions of target systems.

Enterprise systems must guarantee high availability and reliability to provide 24/7 services without interruptions and failures. Mechanisms for handling exceptional cases and implementing fault tolerance techniques can reduce failure occurrences, and increase dependability. Most of such mechanisms address major problems that lead to unexpected service termination or crashes, but do not deal with many subtle domain dependent failures that do not necessarily cause service termination or crashes, but result in incorrect results. In this paper, we propose a technique for developing selfprotecting systems. The technique proposed in this paper observes values at relevant program points. When the technique detects a software failure, it uses the collected information to identify the execution contexts that lead to the failure, and automatically enables mechanisms for preventing future occurrences of failures of the same type. Thus, failures do not occur again after the first detection of a failure of the same type.

Flexibility and interoperability make web services well suited for designing highly-customizable reactive service-based ap-plications, that is interactive applications that can be rapidly adapted to new requirements and environmental conditions. This is the case, for example of personal data managers that many users tailor to their needs to meet different usage con-ditions and requests. In this paper, we propose a model-based approach that provides users with the ability of rapidly developing, adapt-ing and reconfiguring reactive service-based applications to meet new requirements and needs. Users specify their needs by describing sample executions that include interactions with web services through an intuitive interface. Interac-tions are stored in a visual formalism that integrates live sequence charts with graph transformation systems. Mod-els can be visualized, modified, executed and automatically analyzed to identify inconsistencies.

SOQUA 2007 aims to bring together researchers, engineers, and practitioners to discuss and evaluate latest challenges, breakthroughs and experiences in the field of software quality assurance, and to identify open issues and future trends in this area. Among the many quality assurance topics, SOQUA 2007 puts special focus on the role that emerging self adaptive and self-healing solutions can play in quality assurance. The program committee had the difficult task to select 17 papers out of 27 high-quality submissions from all over the world. The selected papers cover 11 countries and 5 continents, and many aspects of software quality assurance, including: self-healing and self-adaptive solutions, testing, quality assurance processes, process modeling, failure analysis and anticipation, quality of requirements, and variability modeling. These papers represent a significant contribution to the state of the art in the field. The workshop program consists of 1 keynote address given by Wilhelm Schäfer, 5 paper sessions hosting the authors' presentations, and 2 discussion sessions on hot-topics in the field.

Component-based technology is increasingly adopted to speed up the development of complex software through component reuse. Unfortunately, the lack of complete information about reused components, and the complex interaction patterns among components can lead to subtle problems that throw new verification challenges. Good components are often re-used many times, sometimes within product lines, in other cases across different products. The reuse of components provides a lot of information that could be useful for verification. In this paper, we show how to automatically analyze component interactions by collecting information about components' behavior during testing and field execution, and then using the collected information for checking the compatibility of components when updated or reused in new products. The paper illustrates the main problems in developing the idea, proposes original solutions, and presents a preliminary experience that illustrates the effectiveness of the approach.

Mobile code solutions can improve the performances of applications over the Internet by reducing the amount of data that must be transferred across the network. The research on genome examines enormous amount of data stored on many distributed databases to retrieve the information relevant for the specific investigation, and thus is likely to greatly benefit for mobile code solutions. This paper studies the benefits of mobile code solutions for research on genome, by comparing different solutions with analytical models, and presenting the results of case studies that allow to identify when mobile code overwhelm client/server solutions. The measured improvements of performance indicate that the retrieval of information from genome databases is a promising domain for mobile code applications.

Autonomic communication and autonomic computing can solve many problems in managing complex network and computer systems, as well as network applications, where computing and networking coexist. Autonomic applications must be able to diagnose and repair their own faults automatically. In particular, they must be able to monitor the execution state, understand the behavior of the application and of the executing environment, and interpret monitored data to identify faults and select a repairing strategy. Assertions have been extensively studied in software engineering for identifying deviations from the expected behaviors and thus signal anomalous outcomes. Unfortunately, classic assertions are defined statically at development time and cannot capture unpredictable changes and evolutions in the execution environment. Thus, they do not easily adapt to autonomic applications. The paper proposes a method for the automatic synthesis and adaptation of assertions from the observed behavior of an application, aimed at achieving adaptive application monitoring. We believe that this represents an important basis to derive autonomic mechanisms that can deal with unpredictable situations.

The article proposes an approach for defining extensible and flexible formal interpreters for diagram notations with significant dynamic semantics. More precisely, it addresses semi-formal diagram notations that have precisely-defined syntax, but informally defined (dynamic) semantics. These notations are often flexible to fit the different needs and expectations of users. Flexibility comes from the incompleteness or informality of the original definition and results in different interpretations.The approach defines interpreters by means of a mapping onto a semantic domain. Two sets of rules define the correspondences between the elements of the diagram notation and those of the semantic domain, and between events and states of the semantic domain and visual annotations on the elements of the diagram notation.Flexibility also leads to notation families, that is, sets of notations that share core concepts, but present slightly different interpretations. Existing approaches usually interpret these notations in isolation; the approach presented in this article allows the interpretation of a family as a whole. The feasibility of the approach is demonstrated through a prototype generator that allows users to implement special-purpose interpreters by defining relatively small sets of rules.

The best approach to testing object-oriented software depends on many factors: the application-under-test, the development approach, the organization of the development and quality assurance teams, the criticality of the application, the development environment and the implementation language(s), the use of design and language features, project timing and resource constraints. Nonetheless, we can outline a general approach that works in stages from independent consideration of classes and their features to consideration of their interactions. A coherent strategy would include three main phases: intraclass, interclass, and system and acceptance testing.

Automation plays an important role in software engineering. ne transition from research breakthroughs to usable tools is neither linear nor easy, and requires a fortunate combination of many elements difficult to identify and merge. In this hard transition process, research prototypes are an important step. They allow researchers to early experience ideas and results on real case studies, and to learn both difficulties in applying new theoretical results and limitations of the theory; and enable practitioners, who can see beyond the frontiers of current state of practice, to identify new technology for improving the software development process and spot advances applicable in the near future.

Estimating software fault-proneness early, i.e., predicting the probability of software modules to be faulty, can help in reducing costs and increasing effectiveness of software analysis and testing. The many available static metrics provide important information, but none of them can be deterministically related to software fault-proneness. Fault-proneness models seem to be an interesting alternative, but the work on these is still biased by lack of experimental validation. This paper discusses barriers and problems in using software fault-proneness in industrial environments, proposes a method for building software fault-proneness models based on logistic regression and cross-validation that meets industrial needs, and provides some experimental evidence of the validity of the proposed approach.

The characteristics of object-oriented software affect type and relevance of faults. In particular the state of the objects may cause faults that cannot be easily revealed with traditional testing techniques. This paper proposes a new technique for interclass testing, that is, the problem of deriving test cases for suitably exercising interactions among clusters of classes. The proposed technique uses data-flow analysis for deriving a suitable set of test case specifications for interclass testing. The paper then shows how to automatically generate feasible test cases that satisfy the derived specifications using symbolic execution and automated deduction. Finally, the paper demonstrates the effectiveness of the proposed technique by deriving test cases for a microscope controller developed for the European Space Laboratory of the Columbus Orbital Facility.

Planning and allocating resources for testing is difficult and it is usually done on empirical basis, often leading to unsatisfactory results. The possibility of early estimating the potential faultiness of software could be of great help for planning and executing testing activities. Most research concentrates on the study of different techniques for computing multivariate models and evaluating their statistical validity, but we still lack experimental data about the validity of such models across different software applications.This paper reports an empirical study of the validity of multivariate models for predicting software fault-proneness across different applications. It shows that suitably selected multivariate models can predict fault-proneness of modules of different software packages.

The effectiveness of the software testing process is a key issue for meeting the increasing demand of quality without augmenting the overall costs of software development. The estimation of software fault-proneness is important for assessing costs and quality and thus better planning and tuning the testing process. Unfortunately, no general techniques are available for estimating software fault-proneness and the distribution of faults to identify the correct level of test for the required quality. Although software complexity and testing thoroughness are intuitively related to the costs of quality assurance and the quality of the final product, single software metrics and coverage criteria provide limited help in planning the testing process and assuring the required quality.By using logistic regression, this paper shows how models can be built that relate software measures and software fault-proneness for classes of homogeneous software products. It also proposes the use of cross-validation for selecting valid models even for small data sets.The early results show that it is possible to build statistical models based on historical data for estimating fault-proneness of software modules before testing, and thus better planning and monitoring the testing activities.

The development of real-time systems is based on a variety of different methods and notations. Despite the purported benefits of formal methods, informal techniques still play a predominant role in current industrial practice. Formal and informal methods have been combined in various ways to smoothly introduce formal methods in industrial practice. The combination of real-time structured analysis (SA-RT) with Petri nets is among the most popular approaches, but has been applied only to requirements specifications. This paper extends SA-RT to specifications of the detailed design of embedded real-time systems, and combines the proposed notation with Petri nets.

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.

Doctoral research in software engineering is a major source of new ideas and of key importance in training scientists for the information technology community. The rapid evolution of information technology is challenging the relevance of doctoral programs in software engineering. These are facing the risk of losing their leading role in training scientists and engineers. Many Universities are threaten by a decreasing number of applications and an increasing number of drop outs. A major goal of the ICSE doctoral workshop, at the turn of the millennium, is to promote doctoral study and provide help and encouragement to those engaged in it. Consequently, the ICSE2000 Doctoral Workshop not only provides a forum for graduate students to present and discuss their dissertation research, it also provides (together with a panel session in the main conference) an opportunity to discuss the role of doctoral research in the new information society. An opening talk by Lee Osterweil is intended to give participants a clear view of both the goal of doctoral research and the methodology with which it is carried out. The presentation of doctoral plans and the open discussion between the committee and the invited students is a unique opportunity to compare PhD programs in different institutions and in different countries. The summary panel scheduled as part of the conference program is designed to open the discussion between the academic and the industrial communities on the role that doctoral research plays in the development and evolution of software engineering.

Programs developed with object technologies have unique features that often make traditional testing methods inadequate. Consider, for instance, the dependence between the state of an object and the behavior of that object: The outcome of a method executed by an object often depends on the state of the object when the method is invoked. It is therefore crucial that techniques for testing of classes exercise class methods when the method's receiver is in different states. The state of an object at any given time depends on the sequence of messages received by the object up to that time. Thus, methods for testing object-oriented software should identify sequences of method invocations that are likely to uncover potential defects in the code under test. However, testing methods for traditional software do not provide this kind of information.

Strong timing requirements and complex interactions with controlled elements complicate the design and validation of software controllers. Different techniques have been proposed to cope with these problems during the different development steps: for example, differential equations for modeling controlled elements, the IEC 1131-3 notations for designing the software controller, and formal models for validating the design, but no definitive solutions have been proposed yet. The paper describes PLCTOOLS, a toolbox that exploits all the aforementioned techniques to supply an integrated environment for the design, formal validation, and automatic code generation of software controllers.

Real-time critical systems require extensive analysis. The potentially considerable damage caused by failures of real-time critical systems justify the use of expensive verification techniques, such as timed reachability analysis. Unfortunately the cost of timed reachability analysis inhibits its systematic application at the early stages of development, when long verification sessions could slow down the development process. Moreover the large reachability space for proving temporal properties reduces the size of specification for which timed reachability analysis can be applied. The authors show how reachability analysis of the nontemporized underlying Petri net can reduce the size of timed reachability analysis. In this way, timed reachability analysis can be used for analyzing industrial-size safety critical systems, paying an acceptable overhead.

Real-time extensions to structured analysis (SA/RT) are popular in industrial practice. Despite the large industrial experience and the attempts to formalize the various “dialects,” SA/RT notations are still imprecise and ambiguous. This article tries to identify the semantic problems of the requirements definition notation defined by Hatley and Pirbhai, one of the popular SA/RT “dialects,” and discusses possible solutions. As opposed to other articles that give their own interpretation, this article does not propose a specific semantics for the notation. This article identifies imprecisions, i.e., missing or partial information about features of the notation; it discusses ambiguities, i.e., elements of the definition that allow at least two different (“reasonable”) interpretations of features of the notation; and it lists extensions, i.e., features not belonging to the notation, but required by many industrial users and often supported by CASE tools. This article contributes by clarifying whether specific interpretations can be given unique semantics or retain ambiguities of the original definition. The article allows for the evaluation of formal definitions by indicating alternatives and consequences of the specific choices.

Health care systems are becoming extremely complex and expensive. New methods are required to optimize health care processes in order to guarantee high quality standards within the (limited) available resources. Resource optimizations able to preserve the quality of treatments require good models of diagnostic and therapeutic processes. This paper proposes LEMMA, a new model for medical processes, that mixes formal and informal notations, overcoming the problems of either approaches. LEMMA merges highly expressive specific constructs with a formal definition. LEMMA has been validated using a prototype for modeling and analyzing diagnostic processes.

Formal specification methods are not often applied in industrial projects, despite their advantages and the maturity of theories and tools.The scarce familiarity of practitioners with formal notations and the difficulties of their use are main causes of the limited success of formal specification methods.Approaches based on the use of popular front-end notations formally defined with mappings on formal models can solve practical problems.However the absence of flexibility of the mappings proposed so far limits the applicability of such approaches to the few environments that match exactly these solutions.This paper presents an original solution based on formalisms to define mappings from front-end notations to formal models.The proposed framework works with different front-end notations and formal models and supports mappings of analysis results obtained on the formal model to the front-end notation chosen by the practitioners.The approach described in this paper has been validated in industrial environments using pilot applications.The paper presents some of the industrial results obtained so far and ongoing experimentations.

State-space analysis techniques have been developed for several representations of concurrent systems, but each tool or technique has typically been targeted to a single design or program notation.We describe an approach to constructing multi-formalism state-space analysis tools for heterogeneous system descriptions, using a shared "inframodel" that represents only the essential information for interpretation by tool components that can be customized to reflect the semantics of each formalism.The (operational) semantics of each formalism, as well as interactions between components described in different formalisms, is described separately through rules governing enabling, matching, and firing of transitions.This results in more natural and compact internal representations, and more efficient analysis, than a purely translational approach.In a previous paper, execution semantics of the inframodel was controlled through a limited set of parameters.The rulebased approach described in this paper accomodates a wider range of state-transition formalisms.

This paper presents a software architecture approach that supports facilities for customizing the set of functionalities offered by CASE systems, without affecting the complexity of the system. The proposed software architecture approach supports on-line composition of elementary and composite functionalities to implement new complex functionalities required for specific applications. The proposal pushes the interesting results obtained by other research groups beyond the goals reached so far by allowing new functionalities to be defined at run-time, without recompiling the system, but relying on dynamic linking mechanisms. The proposal is illustrated with a case-study, successfully used in some industrial pilot projects.

As software evolves from early architectural sketches to final code, a variety of representations are appropriate. Moreover, at most points in development, different portions of a software system are at different stages in development, and consequently in different representations. State-space analysis techniques (reachability analysis, model checking, simulation, etc.) have been developed for several representations of concurrent systems, but each tool or technique has typically been targeted to a single design or program notation.We describe an approach to constructing space analysis tools using a core set of basic representations and components. Such a tool generation approach differs from translation to a common formalism. We need not map every supported design formalism to a single internal form that completely captures the original semantics; rather, a shared "inframodel" represents only the essential information for interpretation by tool components that can be customized to reflect the semantics of each formalism. This results in more natural and compact internal representations, and more efficient analysis, than a purely translational approach.We illustrate the approach by applying the prototype tool to a small example problem, coordination of access to a coffee machine. The coffee machine is controlled by an Ada program, and the protocol of human users is modeled with Petri nets. Nets and process graph models are represented in the common internal form, and their composite behavior is analyzed by the prototype tool.

Rigorous formal methods and intuitive graphical notations can greatly enhance the development of complex computer systems. Formal methods guarantee non-ambiguity and support powerful analysis techniques. Intuitive graphical notations facilitate the communications between engineers preventing errors due to misunderstandings. Unfortunately, tools and techniques based on formal methods do not usually support adequate graphical notations; while tools and methods based on powerful graphical notations often lack formal foundations. This paper proposes a technique that allows kernel formalisms to be accessed through powerful graphical notations. The proposed technique allows graphical notations to be tailored to the needs of the specific application domain. This paper focuses on the tool support.

The problem of analyzing concurrent systems has been investigated by many researchers, and several solutions have been proposed. Among the proposed techniques, reachability analysis—systematic enumeration of reachable states in a finite-state model—is attractive because it is conceptually simple and relatively straightforward to automate and can be used in conjunction with model-checking procedures to check for application-specific as well as general properties. This article shows that the nature of the translation from source code to a modeling formalism is of greater practical importance than the underlying formalism. Features identified as pragmatically important are the representation of internal choice, selection of a dynamic or static matching rule, and the ease of applying reductions. Since combinatorial explosion is the primary impediment to application of reachability analysis, a particular concern in choosing a model is facilitating divide-and-conquer analysis of large programs. Recently, much interest in finite-state verification systems has centered on algebraic theories of concurrency. Algebraic structure can be used to decompose reachability analysis based on a flowgraph model. The semantic equivalence of graph and Petri net-based models suggests that one ought to be able to apply a similar strategy for decomposing Petri nets. We describe how category-theoretic treatments of Petri nets provide a basis for decomposition of Petri net reachability analysis.

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.

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.>

L-Express is a protocol for Local Area Networks based on a single bus topology. It utilizes a simple and efficient virtual token access scheme which provides ordered and collision-free transmission. This paper presents results of measurements performed to investigate in details the behavior of the L-Express protocol under different network speeds, configurations and traffic environments. The measurements are obtained using a mix of simulation and field tests on a network prototype. Voice and integration of voice and data are also taken into account. The results indicate a good behavior (compared with Ethernet) for small size networks (500 m) and Low data rates (10 Mb/s) as well as for Large size networks (5000 m) and high data rates (100 Mb/s)