Tools and algorithms for the construction and analysis of systems

This special section contains the revised and expanded versions of eight of the papers from the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) held in March/April 2004 in Barcelona, Spain. The conference proceedings appeared as volume 2988 in the Lecture Notes in Computer Science series published by Springer. TACAS is a forum for researchers, developers and users interested in rigorously based tools for the construction and analysis of systems. The conference serves to bridge the gaps between different communities – including but not limited to those devoted to formal methods, software and hardware verification, static analysis, programming languages, software engineering, real-time systems, and communications protocols – that share common interests in, and techniques for, tool development. Other more theoretical papers from the conference are collected in a special section of the Theoretical Computer Science journal.     

Introductory paper: scalability aspects of validation

This special section is devoted to a selection of papers that appeared originally in the Proceedings of TACAS 2001, the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems [1] which took place in Genova, Italy in April 2001 as a constituent event of the European joint conferences on theory and Practice of Software. All papers present approaches, tools and algorithms that aim at extending the scope of formal techniques (coverage of systems specifications, data structures, size, and their trade-offs) for validation, verification, and testing of software systems. They are by no means a complete account of the numerous ways in which real software and software systems may become subject to rigorous investigation, but they provide an interesting sampling of novel approaches towards scalability of formal methods-based validation.     

Developments in automated verification techniques

Tools that implement automated verification techniques can be used to fruitfully analyze and validate complex software systems. Developing such tools is an active research area that has produced several promising techniques in the last decade: however, many challenges lie ahead. We briefly review the research area and summarize four papers selected from the Eighteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012).     

Introductory paper

This special section is devoted to a selection of contributions originally presented at the 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002), which took place in Brno, Czech Republic in September 2002 as a satellite event of the 13th conference on concurrency theory (CONCUR 2002). The growing importance of automated formal verification in industry is driving a growing interest in those aspects that have a direct impact on its applicability to real-world problems. One of the main technical challenges is in devising tools that allow one to handle large state spaces. In the last several years numerous approaches to solving this problem have been developed. Recently there has been increasing interest in parallelizing and distributing verification techniques. Papers that appear in this special section provide an interesting sampling of typical approaches in this direction.     

Efficiency of CAMEtools in software quality assurance

Our paper describes the requirements and possibilities of integration of metrics tools in the field of software quality assurance. Tools for the support of the measurement process are herein classified as Computer Assisted Software Measurement and Evaulation Tools (CAMETools). Software measurement regarded as a special type of metrics application provides a great amount of basic information for the evaluation of the software development process or the software product itself. Our paper examines the effectiveness and destination of software measurement in tool-based software development and is based on an analysis of more than 20 CAME tools in the Software Measurement Laboratory at the University of Magdeburg. CAMEtools are useable for the process, product, and resources evaluation in all phases of the software life cycle (including the problem definition) for different development paradigms. The efficiency of CAME tools is described on the basis of a general measurement framework. This framework includes all steps in the software measurement and evaulation process: metrics definition, selection of the evaluation criteria, tool-based modelling and measurement, value presentation and statistical analysis. The framework includes the main aspects of the process evaluation techniques (Capability Maturity Model, ISO 9000-3 etc.) and product evaluation (ISO 9126, etc.). It is not a disjointed set of aspects: our measurement framework represents an incremental technique for the application of quantification of quality aspects in a required quality assurance     

Preface by the section editor

This special section is devoted to some of the novel approaches to hardware-like system verification that are currently being used in industry or the object of fielded research. The topics presented in this special section are based on a selection of the papers which appeared originally in the Proceedings of CHARME 2001, the Eleventh Advanced Research Working Conference on Correct Hardware Design and Verification Methods which took place in Livingston, Scotland, UK in September 2001. They are by no means a complete account of the numerous ways in which hardware and hardware-like systems are being subject to rigorous investigation, but they represent an interesting sample of today’s problems and of the techniques oriented around new uses of verification techniques. Published online: 10 April 2003     

Advances in verification presented in TACAS’13

Computers are becoming increasingly ubiquitous in all aspects of our life. It is becoming more and more important to ensure that the software (and hardware) that drives them performs as expected. Verification is one approach to improve quality of software and hardware. Verification attempts to formally prove that programs or systems fulfill desired properties and lack undesirable properties. This is a thriving area of research, and much resources are invested in extending it both in academia and in industry. In this special issue, we introduce four papers on verification selected from the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13).

     

Improving the effectiveness of system verification

This special section presents three extended and revised papers which originally appeared in the proceedings of the 12th edition of the conference “Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2006” held in Braga, Portugal late March 2006 as a constituent event of the “European joint conferences on Theory and Practice of Software”. All three papers deal with very promising extensions and integrations of formal verification techniques.     

Tools for the construction and analysis of systems

In order to develop reliable software and systems, we depend on practical techniques for the construction and analysis of such software and systems. This special issue of Software Tools for Technology Transfer presents various tool-supported techniques that can help with the construction and analysis of such reliable software and systems. The papers in this special issue are extended versions of selected conference papers from the proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018).

     

Guest Editors' Introduction: GALS Design and Validation

Globally asynchronous, locally synchronous (GALS) design has grown in popularity in both academia and industry. Breaking the synchrony assumption in digital design is often unsettling for designers, and to alleviate the difficulty, researchers in EDA have been proposing various GALS-based solutions. However, the tools, verification techniques, and testing methodologies for asynchronous designs are not as widespread as for synchronous digital design, leading to the hitherto limited usage of GALS design approaches. This special issue introduces some of the basic issues of GALS design and validation in the hardware domain. The hope is that this special issue will generate more interest by researchers and industry practitioners in creating design tools, techniques, and validation methodologies for GALS design.     

Greedy pebbling for proof space compression

International Journal on Software Tools for Technology Transfer - Automated reasoning tools for the verification and synthesis of software often produce proofs to allow independent certification of...     

Special section on Web Systems Evolution

Evolution of Web applications is high for several reasons. Among the others, the need of being constantly updated with the emerging technologies is maybe the most important. Web Systems Evolution is a multifaceted and broad field studying techniques, approaches and tools able to restructure, re-engineer and in general modify a Web application with the intention of renovating or improving some quality aspects of it. This special section is devoted to a selection of papers that have been originally published in the proceedings of the International Symposium on Web Site Evolution, held in Beijing, China in October 2008. The selected papers investigate different issues concerning the evolution of Web Systems, ranging from migration towards SOA to more classic re-engineering and maintenance tasks (e.g., improving the navigational structure). The main contribution of this special section consist of translating some interesting research ideas about Web systems evolution into solutions and tools able to transfer knowledge to the industry.     

Some advances in tools and algorithms for the construction and analysis of systems

Because of the complexity of software systems and their increasing criticality, there is a pressing need for sophisticated and highly automated tools for the analysis of software artifacts and their expected behavioral properties. A growing body of research is using formal methods to produce increasingly powerful and scalable analysis tools, although several challenges still remain. We briefly outline some recent achievements in automated analysis represented by four selected papers from the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). Two of the selected papers describe major achievements in the field of parallel model checking. The third paper presents an auto-active theorem prover for the verification of Eiffel programs. The fourth paper reports on a non-trivial case study with hybrid automata and interactive theorem proving techniques.     

Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020

This special issue of Software Tools for Technology Transfer comprises extended versions of selected papers from the 26th edition of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020). The focus of this conference series is tools and algorithms for the rigorous analysis of software and hardware systems, and the papers in this special cover the spectrum of current work in this field.

     

Guest Editors' Introduction: The State of the Art in Nanoscale CAD

Because of very small feature size, high integration levels, and innovative computational features, new concerns are emerging regarding the implementation of computing systems, leading to increased interest in nanoscale technology. Continued scaling of current top-down trends suggests the need for features measured in the nanometer range. As new techniques to synthesize nanostructures from the bottom up emerge, design practice will require CAD as a framework. Moreover, new tools are necessary for VLSI so that designers can assess the different capabilities for assembling devices into circuits and systems. The design of nanoscale systems is inherently complex and must consider phenomena such as statistical and probabilistic behavior, as well as reduction of parasitic effects. Tools are a necessity to ensure that emerging technologies will move into industry for full commercialization. The convergence of such issues will make CAD at the nanoscale level a vibrant, challenging topic for many years to come. This special section presents a timely account of the state of the art in this area, with emphasis on tools and related frameworks.     

Automatically performing weak mutation with the aid of symbolic execution,concolic testing and search-based testing

Automating software testing activities can increase the quality and drastically decrease the cost of software development. Toward this direction, various automated test data generation tools have been developed. The majority of existing tools aim at structural testing, while a quite limited number aim at a higher level of testing thoroughness such as mutation. In this paper, an attempt toward automating the generation of mutation-based test cases by utilizing existing automated tools is proposed. This is achieved by reducing the killing mutants’ problem into a covering branches one. To this extent, this paper is motivated by the use of state of the art techniques and tools suitable for covering program branches when performing mutation. Tools and techniques such as symbolic execution, concolic execution, and evolutionary testing can be easily adopted toward automating the test input generation activity for the weak mutation testing criterion by simply utilizing a special form of the mutant schemata technique. The propositions made in this paper integrate three automated tools in order to illustrate and examine the method’s feasibility and effectiveness. The obtained results, based on a set of Java program units, indicate the applicability and effectiveness of the suggested technique. The results advocate that the proposed approach is able to guide existing automating tools in producing test cases according to the weak mutation testing criterion. Additionally, experimental results with the proposed mutation testing regime show that weak mutation is able to speedup the mutant execution time by at least 4.79 times when compared with strong mutation.     

基于ASP.NET的安全工器具管理系统的研究与开发

高效准确的安全工器具管理是实现电力企业信息化的重要环节。以ASP.NET和Oracle为技术支持,以B/S模式为架构,用软件工程的指导思想开发安全工器具管理系统。实践证明利用该技术开发的基于Web端的电力企业安全工器具管理系统简单易用,可以很好地提高电力企业安全工器具管理的工作效率和准确性。     

Preface by the section editor

Preliminary versions of the papers of this special section originally appeared in the proceedings of the 6th edition of the conference “Tools and Algorithms for the Construction and Analysis of Systems” (Tacas) held in Berlin early April 2000 as a constituent event of the European joint conferences on Theory and Practice of Software. All papers present tools relevant in the context of systems validation. The first three focus on extensions or particular applications of model-checking techniques, whereas the fourth is about integration of design tools with validation tools, in particular theorem provers and model-checkers. Published online: 24 January 2003     

CADP 2011: a toolbox for the construction and analysis of distributed processes

CADP (Construction and Analysis of Distributed Processes) is a comprehensive software toolbox that implements the results of concurrency theory. Started in the mid-1980s, CADP has been continuously developed by adding new tools and enhancing existing ones. Today, CADP benefits from a worldwide user community, both in academia and industry. This paper presents the latest release, CADP 2011, which is the result of a considerable development effort spanning the last five years. The paper first describes the theoretical principles and the modular architecture of CADP, which has inspired several other recent model checkers. The paper then reviews the main features of CADP 2011, including compilers for various formal specification languages, equivalence checkers, model checkers, compositional verification tools, performance evaluation tools, and parallel verification tools running on clusters and grids. Finally, the paper surveys some significant case studies.     

Tools and algorithms for the construction and analysis of systems: a special issue on tool papers for TACAS 2021

This special issue contains six revised and extended versions of tool papers that appeared in the proceedings of TACAS 2021, the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. The issue is dedicated to the realization of algorithms in tools and the studies of the application of these tools for analysing hard- and software systems.