309 results
Search Results
2. Introductory paper
- Author
-
Stefan Leue and Matthew B. Dwyer
- Subjects
Software model checking ,Programming language ,Computer science ,Algorithmics ,Special section ,computer.software_genre ,computer ,Software ,Information Systems - Published
- 2004
3. Introductory paper
- Author
-
Ofer Strichman and Armin Biere
- Subjects
Computer science ,Engineering ethics ,Software ,Information Systems - Published
- 2005
4. Introduction to the Special Issue devoted to SPIN 2018.
- Author
-
Gallardo, María del Mar and Merino, Pedro
- Subjects
PETRI nets ,COMPUTER science ,SOFTWARE verification ,SOURCE code ,COMPILERS (Computer programs) - Published
- 2020
- Full Text
- View/download PDF
5. Type-based initialization analysis of a synchronous dataflow language.
- Author
-
Colaço, Jean-Louis and Pouzet, Marc
- Subjects
DATA flow computing ,PROGRAMMING languages ,COMPUTER science ,INFORMATION technology ,ELECTRONIC data processing ,TECHNOLOGY - Abstract
One of the appreciated features of the synchronous dataflow approach is that a program defines a perfectly deterministic behavior. But the use of the delay primitive leads to undefined values at the first cycle; thus a dataflow program is really deterministic only if it can be shown that such undefined values do not affect the behavior of the system.This paper presents aninitialization analysisthat guarantees the deterministic behavior of programs. This property being undecidable in general, the paper proposes a safe approximation of the property, precise enough for most dataflow programs. This analysis is aone-bitanalysis - expressions are either initialized or uninitialized - and is defined as an inference-type system with subtyping constraints. This analysis has been implemented in theLucid Synchronecompiler and in a newScade-Lustreprototype compiler at Esterel Technologies. The analysis gives very good results in practice. [ABSTRACT FROM AUTHOR]
- Published
- 2004
- Full Text
- View/download PDF
6. A low-level memory model and an accompanying reachability predicate.
- Author
-
Chatterjee, Shaunak, Lahiri, Shuvendu, Qadeer, Shaz, and Rakamarić, Zvonimir
- Subjects
DATA structures ,COMPUTER science ,SYSTEMS software ,COMPUTER software ,COMPUTER systems - Abstract
Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software. The reachability predicate has already proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. In this paper, we present a memory model suitable for reasoning about low-level pointer operations that is accompanied by a formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present our experience with a prototype verifier on a set of illustrative C benchmarks. [ABSTRACT FROM AUTHOR]
- Published
- 2009
- Full Text
- View/download PDF
7. A systematic classification of security regression testing approaches.
- Author
-
Felderer, Michael and Fourneret, Elizabeta
- Subjects
COMPUTER software security ,INFORMATION technology ,REGRESSION testing (Computer science) ,DIGITAL libraries ,COMPUTER science - Abstract
The openness of modern IT systems and their permanent change make it challenging to keep these systems secure. A combination of regression and security testing called security regression testing, which ensures that changes made to a system do not harm its security, are therefore of high significance and the interest in such approaches has steadily increased. In this article we present a systematic classification of available security regression testing approaches based on a solid study of background and related work to sketch which parts of the research area seem to be well understood and evaluated, and which ones require further research. For this purpose we extract approaches relevant to security regression testing from computer science digital libraries based on a rigorous search and selection strategy. Then, we provide a classification of these according to security regression approach criteria: abstraction level, security issue, regression testing techniques, and tool support, as well as evaluation criteria, for instance evaluated system, maturity of the system, and evaluation measures. From the resulting classification we derive observations with regard to the abstraction level, regression testing techniques, tool support as well as evaluation, and finally identify several potential directions of future research. [ABSTRACT FROM AUTHOR]
- Published
- 2015
- Full Text
- View/download PDF
8. Main issues in protocol testing.
- Author
-
Hogrefe, Dieter
- Subjects
COMPUTER software ,COMPUTER systems ,TELECOMMUNICATION systems ,TELECOMMUNICATION ,COMPUTER science ,TESTING - Abstract
The community of software testing and that of protocol testing are traditionally disjoint. It is seldom the case that protocol testing experts present papers at the large software testing conferences and vice versa. This raises the question about the peculiarities of protocol testing with respect to general software testing. Here we will examine those peculiarities and the consequences in terms of specific methodology developed for protocol testing. [ABSTRACT FROM AUTHOR]
- Published
- 2003
- Full Text
- View/download PDF
9. A verification tool for ERLANG.
- Author
-
Fredlund, Lars-Åke, Gurov, Dilian, Noll, Thomas, Dam, Mads, Arts, Thomas, and Chugunov, Gennady
- Subjects
ERLANG (Computer program language) ,PROGRAMMING languages ,ELECTRONIC data processing ,SOFTWARE verification ,COMPUTER software ,COMPUTER science - Abstract
This paper presents an overview of the main results of the project "Verification of ERLANG Programs", which is funded by the Swedish Business Development Agency (NUTEK) and by Ericsson within the ASTEC (Advanced Software TEChnology) initiative. Its main outcome is the ERLANG Verification Tool (EVT), a theorem prover which assists in obtaining proofs that ERLANG applications satisfy their correctness requirements formulated as behavioural properties in a modal logic with recursion. We give a summary of the verification framework as supported by EVT, discuss reasoning principles essential for successful proofs such as inductive and compositional reasoning, and an efficient treatment of side-effect-free code. The experiences of applying the tool in an industrial case study are summarised, and an approach for supporting verification in the presence of program libraries is outlined. EVT is essentially a classical proof assistant, or theorem-proving tool, requiring users to intervene in the proof process at crucial steps such as stating program in- variants. However, the tool offers considerable support for automatic proof discovery through higher-level tactics tailored to the particular task of the verification of ERLANG programs. In addition, a graphical interface permits easy navigation through proof tableaux, proof reuse, and meaningful feedback about the current proof state, to assist users in taking informed proof decisions. [ABSTRACT FROM AUTHOR]
- Published
- 2003
- Full Text
- View/download PDF
10. Generating online test oracles from temporal logic specificationsTHANKSREF="*"ID="*"This work was supported by VINNOVA within the ASTEC competence center and by Volvo Technical Development Corporation.
- Author
-
Håkansson, John, Jonsson, Bengt, and Lundqvist, Ola
- Subjects
EMBEDDED computer systems ,COMPUTER software ,COMPUTER systems ,COMPUTER logic ,COMPUTER science ,TESTING - Abstract
This paper is concerned with the problem of checking. by means of testing. that a software component satisfies a specification of temporal safety properties. Checking that an actual observed behavior conforms to the specification is performed by a test oracle, which can be either a human tester or a software module. We present a technique for automatically generating test oracles from specifications of temporal safety properties in a metric temporal logic. The logic can express quantitative timing properties. and can also express properties of data values by means of a quantification construct. The generated oracle works online in the sense that checking is performed simultaneously with observation. The technique has been implemented and used in case studies at Volvo Technical Development Corporation. [ABSTRACT FROM AUTHOR]
- Published
- 2003
- Full Text
- View/download PDF
11. Scalable distributed on-the-fly symbolic model checking.
- Author
-
Ben-David, Shoham, Grumberg, Orna, Heyman, Tamir, and Schuster, Assaf
- Subjects
PARALLEL programming ,PARALLEL processing ,ELECTRONIC data processing ,COMPUTER algorithms ,COMPUTER systems ,COMPUTER science - Abstract
This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly model checking for safety properties with a scheme for scalable reachability analysis. We suggest an efficient, BDD-based algorithm for a distributed construction of a counterexample. The extra memory requirement for counterexample generation is evenly distributed among the processes by a memory balancing procedure. At no point during computation does the memory of a single process contain all the data. This enhances scalability. Collaboration between the parallel processes during counterexample generation reduces memory utilization for the backward step. We implemented our method on a standard, loosely-connected environment of workstations, using a high-performance model checker. Our initial performance evaluation, carried out on several large circuits, shows that our method can check models that are too large to fit in the memory of a single node. Our on-the-fly approach may find counterexamples even when the model is too large to fit in the memory of the parallel system. [ABSTRACT FROM AUTHOR]
- Published
- 2003
- Full Text
- View/download PDF
12. From parametric trace slicing to rule systems
- Author
-
Giles Reger and David E. Rydeheard
- Subjects
Correctness ,Scala ,Computer science ,Programming language ,Runtime verification ,020207 software engineering ,02 engineering and technology ,computer.software_genre ,Rotation formalisms in three dimensions ,Theory of computation ,0202 electrical engineering, electronic engineering, information engineering ,Redundancy (engineering) ,020201 artificial intelligence & image processing ,computer ,Software ,Information Systems ,computer.programming_language ,Parametric statistics ,TRACE (psycholinguistics) - Abstract
Parametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper continues our work exploring the relationship between specification techniques for parametric runtime verification. Here we consider the correspondence between trace-slicing automata-based approaches and rule systems. The main contribution is a translation from quantified automata to rule systems, which has been implemented inScala. This then allows us to highlight the key differences in how the two formalisms handle data, an important step in our wider effort to understand the correspondence between different specification languages for parametric runtime verification. This paper extends a previous conference version of this paper with further examples, a proof of correctness, and an optimisation based on a notion of redundancy observed during the development of the translation.
- Published
- 2021
13. Model-based optimization of ARINC-653 partition scheduling
- Author
-
Brian Nielsen, Pujie Han, Ulrik Nyman, and Zhengjun Zhai
- Subjects
Model checking ,Mathematical optimization ,Computer science ,Evolutionary algorithm ,Scheduling (production processes) ,020207 software engineering ,02 engineering and technology ,Parameter space ,Partition (database) ,UPPAAL ,020202 computer hardware & architecture ,Automaton ,Model-based optimization ,Partitioned scheduling ,ARINC 653 ,Theory of computation ,0202 electrical engineering, electronic engineering, information engineering ,Timed automata ,Computer Science::Operating Systems ,Software ,Parameter sweep ,Information Systems - Abstract
The architecture of ARINC-653 partitioned scheduling has been widely applied to avionics systems owing to its robust temporal isolation among applications. However, this partitioning mechanism causes the problem of how to optimize the partition scheduling of a complex system while guaranteeing its schedulability. In this paper, a model-based optimization approach is proposed. We formulate the problem as a parameter sweep application, which searches for the optimal partition scheduling parameters with respect to minimum processor occupancy via an evolutionary algorithm. An ARINC-653 partitioned scheduling system is modeled as a set of timed automata in the model checker UPPAAL. The optimizer tentatively assigns parameter settings to the models and subsequently invokes UPPAAL to verify schedulability as well as evaluate promising solutions. The parameter space is explored with an evolutionary algorithm that combines refined genetic operators and the self-adaptation of evolution strategies. The experimental results show the applicability of our optimization method. The architecture of ARINC-653 partitioned scheduling has been widely applied to avionics systems owing to its robust temporal isolation among applications. However, this partitioning mechanism causes the problem of how to optimize the partition scheduling of a complex system while guaranteeing its schedulability. In this paper, a model-based optimization approach is proposed. We formulate the problem as a parameter sweep application, which searches for the optimal partition scheduling parameters with respect to minimum processor occupancy via an evolutionary algorithm. An ARINC-653 partitioned scheduling system is modeled as a set of timed automata in the model checker UPPAAL. The optimizer tentatively assigns parameter settings to the models and subsequently invokes UPPAAL to verify schedulability as well as evaluate promising solutions. The parameter space is explored with an evolutionary algorithm that combines refined genetic operators and the self-adaptation of evolution strategies. The experimental results show the applicability of our optimization method.
- Published
- 2021
14. Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2019
- Author
-
Lijun Zhang and Tomáš Vojnar
- Subjects
Software ,business.industry ,Computer science ,Theory of computation ,Technology transfer ,Subject (documents) ,business ,Formal verification ,Algorithm ,Information Systems - Abstract
Automated techniques and tools for the construction and analysis of systems are inevitable to manage the complexity of the current systems. Such techniques and tools are the subject of interest of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems—TACAS. This special issue of Software Tools for Technology Transfer presents extended versions of five selected papers from the 25th edition of TACAS that took place in 2019. All of the papers included into this special issue aim at various aspects of automated design and formal verification and hence contribute to development of more reliable computer systems.
- Published
- 2021
15. Automating deductive verification for weak-memory programs (extended version)
- Author
-
Alexander J. Summers and Peter Müller
- Subjects
Weak consistency ,Computer science ,Programming language ,020207 software engineering ,02 engineering and technology ,Separation logic ,C11 ,Permission ,Mathematical proof ,computer.software_genre ,Encoding (memory) ,0202 electrical engineering, electronic engineering, information engineering ,Memory model ,computer ,Software ,Information Systems ,Abstraction (linguistics) - Abstract
Writing correct programs for weak-memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of such programs have recently been proposed, but their usage has been limited thus far to manual proofs. Automating proofs in these logics via first-order solvers is non-trivial, due to features such as higher-order assertions, modalities and rich permission resources. In this paper, we provide the first encoding of a weak-memory program logic using existing deductive verification tools. Our work enables, for the first time, the (unbounded) verification of C11 programs at the level of abstraction provided by the program logics; the only necessary user interaction is in the form of specifications written in the program logic and, in rare cases, ghost operations. We tackle three recent program logics: Relaxed Separation Logic and two forms of Fenced Separation Logic, and show how these can be encoded using the Viper verification infrastructure. In doing so, we illustrate several novel encoding techniques which could be employed for other logics. Our work is implemented, and has been evaluated on examples from existing papers as well as the Facebook open-source Folly library.
- Published
- 2020
16. Learning Moore machines from input–output traces
- Author
-
Georgios Giantamidis, Stavros Tripakis, and Stylianos Basagiannis
- Subjects
Mealy machine ,Finite-state machine ,Learning automata ,Computer science ,business.industry ,Moore machine ,Automaton ,Theory of computation ,Artificial intelligence ,Equivalence (formal languages) ,business ,Equivalence (measure theory) ,Software ,Information Systems - Abstract
The problem of learning automata from example traces (but no equivalence or membership queries) is fundamental in automata learning theory and practice. In this paper we study this problem for finite state machines with inputs and outputs, and in particular for Moore machines. We develop three algorithms for solving this problem: (1) the PTAP algorithm, which transforms a set of input-output traces into an incomplete Moore machine and then completes the machine with self-loops; (2) the PRPNI algorithm, which uses the well-known RPNI algorithm for automata learning to learn a product of automata encoding a Moore machine; and (3) the MooreMI algorithm, which directly learns a Moore machine using PTAP extended with state merging. We prove that MooreMI has the fundamental identification in the limit property. We also compare the algorithms experimentally in terms of the size of the learned machine and several notions of accuracy, introduced in this paper. Finally, we compare with OSTIA, an algorithm that learns a more general class of transducers, and find that OSTIA generally does not learn a Moore machine, even when fed with a characteristic sample.
- Published
- 2019
17. Configuration of inter-process communication with probabilistic model checking
- Author
-
Christel Baier, Hermann Härtig, Martin Küttler, Linda Herrmann, Sascha Klüppelholz, and Tobias Stumpf
- Subjects
Optimality criterion ,Computer science ,020207 software engineering ,Fault tolerance ,02 engineering and technology ,Interval (mathematics) ,computer.software_genre ,Inter-process communication ,Theory of computation ,0202 electrical engineering, electronic engineering, information engineering ,Markov decision process ,Communications protocol ,Algorithm ,computer ,Software ,Information Systems ,Parametric statistics - Abstract
Ever-increasing bit flip rates caused by shrinking hardware tiles increase the demand for resilient systems. In particular, safety- and functionality-critical system parts need to be protected. Inter-process communication is one such critical part. Applying fault tolerance techniques often comes with a configuration problem, since real-world systems typically have tunable system parameters. These need to be configured with respect to certain optimality criterion. The paper addresses the parameter synthesis problem for inter-process communication protocols that are affected by bit flips. Tunable parameters are the probability of error detection and the expected time interval between system refresh. We provide a tool that automatically generates a model of bit-flip-prone inter-process communication for a given set of processes and their communication structure. The tool is used to exemplarily generate a model of a space probe. Parametric extensions of probabilistic model checking are applied to obtain rational functions for the availability of the space probe and other characteristics. We find a configuration setting that maximizes availability and investigates side effects for this configuration. The paper also compares exemplarily for the space probe model the most-standard probabilistic model checking methods (value iteration, interval iteration, and exact model checking) with respect to their time consumption and accuracy and reveals complexity concerns arising when evaluating the rational functions.
- Published
- 2019
18. Tools for the construction and analysis of systems
- Author
-
Dirk Beyer and Marieke Huisman
- Subjects
Deductive verification ,Computer science ,02 engineering and technology ,Cyber-physical system ,Statistical model checking ,Software ,0202 electrical engineering, electronic engineering, information engineering ,Safety analysis ,Quantitative analysis ,Reactive system ,business.industry ,Hyperproperty ,020207 software engineering ,Refinement ,Quantitative analysis (finance) ,Theory of computation ,Technology transfer ,020201 artificial intelligence & image processing ,Runtime analysis ,Software engineering ,business ,Weak-memory model ,Information Systems - Abstract
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).
- Published
- 2020
19. Model-based testing of apps in real network scenarios
- Author
-
Laura Panizo, Bruno García, and Almudena Díaz
- Subjects
Model checking ,Model-based testing ,Computer science ,business.industry ,Testbed ,020207 software engineering ,Manual testing ,02 engineering and technology ,User experience design ,0202 electrical engineering, electronic engineering, information engineering ,Cellular network ,Android (operating system) ,business ,Software engineering ,Software ,5G ,Information Systems - Abstract
Traditional testing methods for mobile apps focus on detecting execution errors. However, the evolution of mobile networks toward 5G will require additional support for app developers to also ensure good performance and user experience. Manual testing in a number of scenarios is not enough to satisfy the expectations of the apps’ end users. This paper presents the testing framework developed in the TRIANGLE project (https://www.triangle-project.eu/), which integrates a complete mobile network testbed to test, benchmark and certify mobile apps. In this paper, we focus on a recent extension of the TRIANGLE framework that uses model-based testing based on model checking to support the automatic generation of user interactions. We introduce the complete testing framework and the basis of the model-based extension. Finally, we use the testing framework to evaluate the performance of the ExoPlayer app in different network scenarios. ExoPlayer is a video streaming app for Android that implements different adaptive streaming protocols.
- Published
- 2019
20. ASAP: A Source Code Authorship Program
- Author
-
Matthew F. Tennyson
- Subjects
Source code ,Information retrieval ,Computer program ,business.industry ,Computer science ,Nearest neighbor search ,media_common.quotation_subject ,Interface (computing) ,Copyright infringement ,ComputingMilieux_LEGALASPECTSOFCOMPUTING ,Task (project management) ,Software ,Plagiarism detection ,business ,Information Systems ,media_common - Abstract
Source code authorship attribution is the task of determining who wrote a computer program, based on its source code, usually when the author is either unknown or under dispute. Areas where this can be applied include software forensics, cases of software copyright infringement, and detecting plagiarism. Numerous methods of source code authorship attribution have been proposed and studied. However, there are no known easily accessible and user-friendly programs that perform this task. Instead, researchers typically develop software in an ad hoc manner for use in their studies, and the software is rarely made publicly available. In this paper, we present a software tool called A Source Code Authorship Program (ASAP), which is suitable to be used by either the layperson or the expert. An author can be attributed to individual documents one at a time, or complex authorship attribution experiments can easily be performed on large datasets. In this paper, the interface and implementation of the ASAP tool is presented, and the tool is validated by using it to replicate previously published authorship attribution experiments.
- Published
- 2019
21. Towards formal methods diversity in railways: an experience report with seven frameworks
- Author
-
Alessio Ferrari, Franco Mazzanti, and Giorgio Oronzo Spagnolo
- Subjects
Model checking ,Formal methods diversity ,Computer science ,02 engineering and technology ,0202 electrical engineering, electronic engineering, information engineering ,Experience report ,Equivalence (formal languages) ,Architecture ,computer.programming_language ,business.industry ,CBTC ,Deadlock avoidance ,020207 software engineering ,Formal methods ,Rotation formalisms in three dimensions ,Train scheduling ,CPN Tools ,Promela ,Theory of computation ,020201 artificial intelligence & image processing ,Railways ,Software engineering ,business ,computer ,Software ,Automatic train protection ,Information Systems - Abstract
In the ever expanding universe of formal methods, several tools exist that can be exploited to validate early system designs, and that are applicable to problems of the railway domain. In this paper, we present an experience report in formal modelling and verification using seven different formal environments, namely UMC, Promela/SPIN, NuSMV, mCRL2, CPN Tools, FDR4 and CADP. In particular, we model and verify an algorithm that addresses a typical railway problem, namely deadlock avoidance in train scheduling. The algorithm is designed according to a prototypical architecture, the so-called blackboard pattern, in which a set of global data are atomically updated by a set of concurrent guarded agents. Our experience, limited to the specific problem, shows that the design of the algorithm can be translated into the different formalisms with acceptable effort, while deep proficiency with the tools is required to optimise the performance. The current paper establishes the preliminary foundations for the concept of formal methods diversity in the development of railway systems. The concept is based on the idea that if different non-certified formal environments are used to verify the same design, this increases the confidence on the verification results. Furthermore, by checking that the number of states generated during the verification process is the same for each framework, the designer can have an initial indication of the equivalence of the diverse models. The industrial application of this promising concept requires further research, and appropriate guidelines shall be established to identify the proper formal environments to use for a specific railway problem, and to define an industrial process in which formal methods diversity can be exploited at its full benefits. The paper presents the different models developed, compares the tools employed in terms of language features and performance, and discusses the industrial implications of the concept of formal methods diversity in the railway domain.
- Published
- 2018
22. Some advances in tools and algorithms for the construction and analysis of systems
- Author
-
Christel Baier and Cesare Tinelli
- Subjects
Model checking ,Computer science ,business.industry ,Proof assistant ,020207 software engineering ,02 engineering and technology ,Formal methods ,Eiffel ,Automated theorem proving ,Automated proof checking ,Theory of computation ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,Software system ,Software engineering ,business ,Algorithm ,computer ,Software ,Information Systems ,computer.programming_language - Abstract
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.
- Published
- 2017
23. Greedy pebbling for proof space compression
- Author
-
Bruno Woltzenlogel Paleo and Andreas Fellner
- Subjects
Sequence ,Correctness ,Computer science ,020207 software engineering ,02 engineering and technology ,Resolution (logic) ,Mathematical proof ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Theory of computation ,0202 electrical engineering, electronic engineering, information engineering ,Topological sorting ,Automated reasoning ,Heuristics ,Algorithm ,Software ,Information Systems - Abstract
Automated reasoning tools for the verification and synthesis of software often produce proofs to allow independent certification of the correctness of the produced solutions. As proofs can be large, this paper considers the problem of compressing proofs with respect to their space, which is approximately proportional to the memory necessary to check them. Proof checking with a small amount of available memory is analogous to playing a pebbling game with a small number of pebbles. This paper exploits this analogy and describes novel algorithms for playing a pebbling game. The sequence of moves executed in the pebbling game then corresponds to an improved topological ordering of the nodes of the proof, leading to smaller memory consumption when the proof is checked. Because the number of possible pebbling strategies and topological orderings is too large, brute-force approaches to find optimal solutions are impractical, and hence, the new pebbling algorithms proposed here are based on heuristics for finding good, though not necessarily optimal, solutions. The algorithms are evaluated on the task of compressing the space of thousands of propositional resolution proofs generated by SAT- and SMT-solvers.
- Published
- 2017
24. The physics of software tools: SWOT analysis and vision
- Author
-
Bernhard Steffen
- Subjects
Model checking ,business.industry ,Computer science ,Scientific progress ,Runtime verification ,020207 software engineering ,02 engineering and technology ,Static analysis ,Software ,Conceptual design ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,Software engineering ,business ,SWOT analysis ,Information Systems ,Coding (social sciences) - Abstract
This paper reviews the seemingly inevitable trend that software tools are no longer just a means for supporting the design, construction, and analysis of (large-scale) systems, but become so complex that each of them turns into a reality of their own, with its own "physics", that needs to be studied in its own right. The true effects of combining methodologies as diverse as classical static analysis, model checking, SAT and SMT solving, and dynamic methods such as simulation, runtime verification, testing, and learning, with their dedicated means of optimizations in terms of, e.g., BDD coding, parallelization, and various forms of abstraction and reduction, are very dependent on the particular tools and typically hardly predictable. Corresponding experimental investigations, today often supported by diverse and frequent tool challenges, provide interesting indications about the applied technology, but typically fail to provide sufficient evidence to transfer results to other settings and tools. Moreover, implementation-specific details often dominate the observed effects which thereby become invalid for drawing conceptual conclusions. On the other hand, requiring consequent in-depth analysis of any experimental observation in order to pinpoint the underlying conceptual consequences before publication would slow down the scientific exchange and also hinder the scientific progress. This paper analyzes the situation of today's software tools from a global perspective in terms of a SWOT (Strength, Weaknesses, Opportunities, Treats) analysis, identifies challenges, and establishes a global vision for overcoming current weaknesses.
- Published
- 2017
25. TSTL: the template scripting testing language
- Author
-
James O’Brien, Jervis Pinto, Pooria Azimi, Pranjal Mittal, Kevin Kellar, Alex Groce, and Josie Holmes
- Subjects
Model-based testing ,Programming language ,Computer science ,business.industry ,White-box testing ,020207 software engineering ,Manual testing ,02 engineering and technology ,computer.software_genre ,Test harness ,Test case ,System under test ,020204 information systems ,0202 electrical engineering, electronic engineering, information engineering ,Exploratory testing ,Test Management Approach ,Software engineering ,business ,computer ,Software ,Information Systems - Abstract
A test harness, in automated test generation, defines the set of valid tests for a system, as well as their correctness properties. The difficulty of writing test harnesses is a major obstacle to the adoption of automated test generation and model checking. Languages for writing test harnesses are usually tied to a particular tool and unfamiliar to programmers, and often limit expressiveness. Writing test harnesses directly in the language of the software under test (SUT) is a tedious, repetitive, and error-prone task, offers little or no support for test case manipulation and debugging, and produces hard-to-read, hard-to-maintain code. Using existing harness languages or writing directly in the language of the SUT also tends to limit users to one algorithm for test generation, with little ability to explore alternative methods. In this paper, we present TSTL, the template scripting testing language, a domain-specific language (DSL) for writing test harnesses. TSTL compiles harness definitions into an interface for testing, making generic test generation and manipulation tools for all SUTs possible. TSTL includes tools for generating, manipulating, and analyzing test cases, including simple model checkers. This paper motivates TSTL via a large-scale testing effort, directed by an end-user, to find faults in the most widely used geographic information systems tool. This paper emphasizes a new approach to automated testing, where, rather than focus on developing a monolithic tool to extend, the aim is to convert a test harness into a language extension. This approach makes testing not a separate activity to be performed using a tool, but as natural to users of the language of the system under test as is the use of domain-specific libraries such as ArcPy, NumPy, or QIIME, in their domains. TSTL is a language and tool infrastructure, but is also a way to bring testing activities under the control of an existing programming language in a simple, natural way.
- Published
- 2016
26. Model-based software quality assurance tools and techniques presented at FASE 2018
- Author
-
Alessandra Russo and Andy Schürr
- Subjects
Software quality assurance ,Computer science ,business.industry ,0202 electrical engineering, electronic engineering, information engineering ,020207 software engineering ,02 engineering and technology ,Software engineering ,business ,Theme (computing) ,Quality assurance ,Software ,Information Systems - Abstract
This special issue contains revised and substantially extended versions of a few of the best papers presented at FASE 2018. These papers share one common theme, the development of new model-based software quality assurance methods, and cover a substantial section of the whole spectrum of today available quality assurance tools and techniques.
- Published
- 2019
27. A general model checking framework for various memory consistency models
- Author
-
Tatsuya Abe and Toshiyuki Maeda
- Subjects
Model checking ,Sequential access memory ,Multi-core processor ,Global address space ,Weak consistency ,Theoretical computer science ,Sequential consistency ,Programming language ,Computer science ,Release consistency ,Strong consistency ,Eventual consistency ,Consistency model ,020207 software engineering ,Causal consistency ,02 engineering and technology ,computer.software_genre ,0202 electrical engineering, electronic engineering, information engineering ,Local consistency ,020201 artificial intelligence & image processing ,Partitioned global address space ,Coarray Fortran ,computer ,Software ,Information Systems - Abstract
Relaxed memory consistency models are common and essential when multiple processes share a single global address space, such as when using multicore CPUs, distributed shared-memory programming languages, and so forth. Programming within these models is difficult and error prone, because of non-intuitive behaviors that could not occur in a strict consistency model. In addition, because the memory consistency models vary from language to language, and CPU to CPU, a program that may work correctly on one system may not work on another. To address the problem, this paper describes a model checking framework in which users are able to check their programs under various memory consistency models. More specifically, our framework provides a base model that exhibits very relaxed behaviors, and users are able to define various consistency models by adding constraints to the base model. This paper also describes McSPIN, a prototype implementation of a model checker based on the proposed framework. McSPIN can take a memory consistency model as an input, as well as a program and a property to be checked. We have specified the necessary constraints for three practical existing memory consistency models (Unified Parallel C, Coarray Fortran, and Itanium). McSPIN verified some example programs correctly, and confirmed the expected differences among the three models.
- Published
- 2016
28. Advances in test generation for testing software and systems
- Author
-
Hüsnü Yenigün, Cemal Yilmaz, and Andreas Ulrich
- Subjects
Test strategy ,business.industry ,Computer science ,020207 software engineering ,Software performance testing ,02 engineering and technology ,Software quality assurance ,Acceptance testing ,020204 information systems ,Software construction ,0202 electrical engineering, electronic engineering, information engineering ,Test Management Approach ,Software reliability testing ,Software engineering ,business ,System integration testing ,Software ,Information Systems - Abstract
Among the software quality assurance techniques, testing stands out as one of the most frequently used techniques in practice. Consequently, testing is also widely studied in research. An important aspect in testing that receives much attention is the problem of automated test generation. This introductory paper summarizes the papers selected from the 25th IFIP International Conference on Testing Software and Systems (ICTSS 2013), which all deal with this topic. The field is briefly introduced by pointing out to some of the existing survey articles and relating the selected papers in this issue to each other and to the known body of knowledge.
- Published
- 2015
29. Systematic synthesis of delta modeling languages
- Author
-
Klaus Müller, Bernhard Rumpe, Arne Haber, Katrin Hölldobler, Markus Look, Christoph Schulze, Ina Schaefer, Carsten Kolassa, and Publica
- Subjects
Domain-specific language ,Grammar ,Programming language ,Modeling language ,Computer science ,business.industry ,media_common.quotation_subject ,Context (language use) ,computer.software_genre ,Transformation language ,Language primitive ,Rule-based machine translation ,Artificial intelligence ,Software product line ,business ,computer ,Software ,Natural language processing ,Information Systems ,media_common - Abstract
Delta modeling is a modular, yet flexible approach to capture variability by explicitly representing differences between system variants or versions. The conceptual idea of delta modeling is language-independent. But, to apply delta modeling to a concrete language, either a generic transformation language has to be used or the corresponding delta language has to be manually developed for each considered base language. Generic languages and their tool support often lack readability and specific context condition checking, since they are unrelated to the base language. In this paper, we present a process that allows synthesizing a delta language from the grammar of a given base language. Our method relies on an automatically generated language extension that can be manually adapted to meet domain-specific needs. We illustrate our method using delta modeling on a textual variant of architecture diagrams. Furthermore, we evaluate our method using a comparative case study. This case study covers an architectural, a structural, and a behavioral language and compares the preexisting handwritten grammars to the generated grammars as well as the manually tailored grammars. This paper is an extension of Haber et al. (Proceedings of the 17th international software product line conference (SPLC'13), pp 22---31, 2013).
- Published
- 2015
30. FDR3: a parallel refinement checker for CSP
- Author
-
A. W. Roscoe, Thomas Gibson-Robinson, Alexandre Boulgakov, and Philip Armstrong
- Subjects
Model checking ,Speedup ,Computer science ,business.industry ,020207 software engineering ,Cloud computing ,02 engineering and technology ,Construct (python library) ,Parallel computing ,Supercomputer ,Divergence (computer science) ,Theory of computation ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,Representation (mathematics) ,business ,Algorithm ,Software ,Information Systems - Abstract
Failures divergence refinement 3 (FDR3) is a complete rewrite of the CSP refinement checker FDR2 that incorporates a significant number of enhancements. In this paper, we describe the operation of FDR3 at a high level and give a detailed description of several of the more important innovations. FDR3 has a new parallel refinement-checking algorithm that is able to achieve a near linear speedup as the number of cores increases. This algorithm scales linearly not only on shared-memory systems, but also on distributed systems (i.e. clusters). In particular, this paper presents experimental results that show FDR3 can achieve a speedup factor in excess of 1000 versus the sequential case on a cluster of 64, 16-core machines (i.e. 1024 cores): we obtain similar performance improvements on a supercomputer and, more interestingly, on a commodity cloud computing provider. We also present experimental results that compare FDR3 to related tools, and indicate that (as far as we know) FDR3 is unique in being able to scale beyond the bounds of main memory. This paper also describes the new algorithm that FDR3 uses to construct its internal representation of CSP processes, one of the key problems to solve in order to efficiently model-check process algebras.
- Published
- 2015
31. How to model and prove hybrid systems with KeYmaera: a tutorial on safety
- Author
-
Sarah M. Loos, Jan-David Quesel, Stefan Mitsch, Nikos Arechiga, and André Platzer
- Subjects
0209 industrial biotechnology ,Theoretical computer science ,business.industry ,Computer science ,020207 software engineering ,Context (language use) ,02 engineering and technology ,Gas meter prover ,Formal methods ,Automated theorem proving ,020901 industrial engineering & automation ,Hybrid system ,Theory of computation ,0202 electrical engineering, electronic engineering, information engineering ,Software engineering ,business ,Formal verification ,Software ,Dynamic logic (digital electronics) ,Information Systems - Abstract
This paper is a tutorial on how to model hybrid systems as hybrid programs in differential dynamic logic and how to prove complex properties about these complex hybrid systems in KeYmaera, an automatic and interactive formal verification tool for hybrid systems. Hybrid systems can model highly nontrivial controllers of physical plants, whose behaviors are often safety critical such as trains, cars, airplanes, or medical devices. Formal methods can help design systems that work correctly. This paper illustrates how KeYmaera can be used to systematically model, validate, and verify hybrid systems. We develop tutorial examples that illustrate challenges arising in many real-world systems. In the context of this tutorial, we identify the impact that modeling decisions have on the suitability of the model for verification purposes. We show how the interactive features of KeYmaera can help users understand their system designs better and prove complex properties for which the automatic prover of KeYmaera still takes an impractical amount of time. We hope this paper is a helpful resource for designers of embedded and cyber–physical systems and that it illustrates how to master common practical challenges in hybrid systems verification.
- Published
- 2015
32. Approximate planning and verification for large Markov decision processes
- Author
-
Sylvain Peyronnet, Richard Lassaigne, Équipe de Logique Mathématique (ELM), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Equipe AMACC - Laboratoire GREYC - UMR6072, Groupe de Recherche en Informatique, Image et Instrumentation de Caen (GREYC), Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Ingénieurs de Caen (ENSICAEN), Normandie Université (NU)-Normandie Université (NU)-Université de Caen Normandie (UNICAEN), Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Ingénieurs de Caen (ENSICAEN), and Normandie Université (NU)
- Subjects
Mathematical optimization ,Markov kernel ,Theoretical computer science ,Computer science ,0211 other engineering and technologies ,Markov process ,02 engineering and technology ,Markov model ,ComputingMethodologies_ARTIFICIALINTELLIGENCE ,Continuous-time Markov chain ,symbols.namesake ,Markov renewal process ,Reachability ,Markov algorithm ,Convergence (routing) ,0202 electrical engineering, electronic engineering, information engineering ,State space ,[INFO]Computer Science [cs] ,ComputingMilieux_MISCELLANEOUS ,Markov blanket ,021103 operations research ,Markov chain ,Variable-order Markov model ,Probabilistic logic ,Partially observable Markov decision process ,020207 software engineering ,Theory of computation ,symbols ,Markov property ,020201 artificial intelligence & image processing ,Markov decision process ,Software ,Information Systems - Abstract
We focus on the planning and verification problems for very large probabilistic systems, such as Markov decision processes (MDPs), from a complexity point of view. More precisely, we deal with the problem of designing an efficient approximation method to compute a near-optimal policy for the planning problem in discounted MDPs and the satisfaction probabilities of interesting properties, like reachability or safety, over the Markov chain obtained by restricting the MDP to the near-optimal policy. In this paper, we present two different approaches. The first one is based on sparse sampling while the second uses a variant of the multiplicative weights update algorithm. The complexity of the first approximation method is independent of the size of the state space and uses only a probabilistic generator of the MDP. We give a complete analysis of this approach, for which the control parameter is mainly the targeted quality of the approximation. The second approach is more prospective and is different in the sense that the method can be controlled dynamically by observing its speed of convergence. Parts of this paper have already been presented in Lassaigne and Peyronnet (in Proceedings of the ACM Symposium on applied computing, SAC 2012, pp 1314---1319, ACM 2012), by the same authors.
- Published
- 2014
33. Statistical model checking for biological applications
- Author
-
Paolo Zuliani
- Subjects
FOS: Computer and information sciences ,Computer Science - Logic in Computer Science ,Theoretical computer science ,Relation (database) ,Computer science ,Stochastic modelling ,Systems and Control (eess.SY) ,Quantitative Biology - Quantitative Methods ,Logic in Computer Science (cs.LO) ,Gillespie algorithm ,FOS: Biological sciences ,Ordinary differential equation ,Stochastic simulation ,Theory of computation ,FOS: Electrical engineering, electronic engineering, information engineering ,Computer Science - Systems and Control ,Focus (optics) ,Literature survey ,Quantitative Methods (q-bio.QM) ,Software ,Information Systems - Abstract
In this paper, we survey recent work on the use of statistical model checking techniques for biological applications. We begin with an overview of the basic modelling techniques for biochemical reactions and their corresponding stochastic simulation algorithm--the Gillespie algorithm. We continue by giving a brief description of the relation between stochastic models and continuous (ordinary differential equation) models. Next, we present a literature survey, divided into two general areas. In the first area, we focus on works addressing verification of biological models, while in the second area we focus on papers tackling the parameter synthesis problem. We conclude with some open problems and directions for further research.
- Published
- 2014
34. On piggyback runtime monitoring of object-oriented programs
- Author
-
Raphaël Tremblay-Lessard, Jason Vallet, and Sylvain Hallé
- Subjects
Object-oriented programming ,Finite-state machine ,Computer science ,Distributed computing ,Runtime Callable Wrapper ,Real-time computing ,Process (computing) ,Code (cryptography) ,Overhead (computing) ,State (computer science) ,Object (computer science) ,Software ,Information Systems - Abstract
A runtime monitor enforcing a constraint on sequences of method calls on an object involves the implementation of an independent piece of code called a monitor. This monitor intercepts relevant events in the program and must keep track of the state of the sequence by updating an appropriate state machine. The present paper stems from the observation that an object's member fields must already contain an encoding of that state machine and that a monitor essentially duplicates operations that the object performs internally. Rather than maintaining a state machine in parallel, the paper puts forward the concept of "piggyback" runtime monitoring, where the monitor relies as much as possible on the object's own state variables to perform its task. Experiments on real-world benchmarks show that this approach greatly simplifies the monitoring process and drastically reduces the incurred runtime overhead compared to classical solutions.
- Published
- 2014
35. Functional prototypes for generic C++ libraries: a transformational approach based on higher-order, typed signatures
- Author
-
Sibylle Schupp, Cezar Ionescu, and Daniel Lincke
- Subjects
Theoretical computer science ,Generic programming ,Computer science ,Programming language ,Program transformation ,Context (language use) ,computer.software_genre ,Kernel (linear algebra) ,Transformation (function) ,Theory of computation ,Haskell ,computer ,Software ,Defunctionalization ,Information Systems ,computer.programming_language - Abstract
This paper presents a method for developing generic C++ software libraries from functional prototypes, based on program transformation. More precisely, the type signatures of generic functions, i.e., functions parameterized on types, are transformed. This transformation maps type-level expressions from functional higher-order, typed languages to type-level expressions in C++. In particular, type-level functional constructs such as higher-order functions and type constructors, are mapped to type parameters of generics that are constrained with appropriate concepts. The core of the transformation is a novel form of "defunctionalization" at the level of types. To make the transformation retargetable, we based it on two kernel languages that can be bound to different functional and object-oriented languages. For this paper, we use bindings to Haskell as front end and C++ with concepts as back end. Our transformational approach presents an alternative to a language extension and is useful particularly for functional prototyping where functional features are employed at specification time. We illustrate our approach by a case study: we show how we developed a generic C++ library for vulnerability modeling in the context of global change from a functional prototype in Haskell.
- Published
- 2014
36. Formally based tool support for model checking Erlang applications
- Author
-
John Derrick and Qiang Guo
- Subjects
Model checking ,Functional programming ,business.industry ,Programming language ,Computer science ,Concurrency ,Process calculus ,Algebraic specification ,Erlang (programming language) ,computer.software_genre ,Embedded system ,Programming paradigm ,Systems design ,business ,computer ,Software ,Information Systems ,computer.programming_language - Abstract
Model checking as a verification technique has proved effective at the system design and hardware level, and is now beginning to be applied to program code. In this paper, we study the application of model checking techniques in the development of Erlang systems. Erlang is a concurrent functional language with specific support for the development of distributed, fault-tolerant systems with soft real-time requirements. It was designed from the start to support a concurrency-oriented programming paradigm and large distributed implementations that this supports. The methodology we describe in this paper consists of abstracting the behaviour of Erlang and OTP components into a process algebraic specification, specifically an mCRL2 specification, upon which the standard model checker CADP can be used to verify the system’s properties. In addition to rules that model the Erlang syntax, a translation mechanism for the OTP modules gen_server, supervisor and gen_fsm, and the timeout event are defined. A tool-set etomcrl2 has been developed to automate the process of translation. A small illustrative example is used to evaluate the effectiveness of the proposed techniques, and its results show that the proposed techniques are effective in both verifying properties as well as distinguishing between correct and faulty implementations of the design.
- Published
- 2010
37. Synthesizing switching logic using constraint solving
- Author
-
Ashish Tiwari, Ankur Taly, and Sumit Gulwani
- Subjects
Constraint (information theory) ,Mathematical optimization ,Logic synthesis ,Computer science ,Hybrid system ,Constraint logic programming ,Hybrid algorithm (constraint satisfaction) ,Invariant (mathematics) ,Topology ,Software ,Satisfiability ,Information Systems ,Decidability - Abstract
For a system that can operate in multiple different modes, we define the switching logic synthesis problem as follows: given a description of the dynamics in each mode of the system, find the conditions for switching between the modes so that the resulting system satisfies some desired properties. In this paper, we present an approach for solving the switching logic synthesis problem in the case when (1) the dynamics in each mode of the system are given using differential equations and, hence, the synthesized system is a hybrid system, and (2) the desired property is a safety property. Our approach for solving the switching logic synthesis problem, called the constraint-based approach, consists of two steps. In the first constraint generation step, the synthesis problem is reduced to satisfiability of a quantified formula over the theory of reals. In the second constraint solving step, the quantified formula is solved. This paper focuses on constraint generation. The constraint generation step is based on the concept of a controlled inductive invariant. The search for controlled inductive invariant is cast as a constraint solving problem. The controlled inductive invariant is then used to arrive at the maximally liberal switching logic. We prove that the synthesized switching logic always gives us a well-formed and safe hybrid system. When the system, the safety property, and the controlled inductive invariant are all expressed only using polynomials, the generated constraint is an $${\exists\forall}$$ formula in the theory of reals, whose satisfiability is decidable.
- Published
- 2010
38. Evaluation of Kermeta for solving graph-based problems
- Author
-
Sagar Sen, Cyril Faucher, Jean-Marc Jézéquel, Olivier Barais, and Naouel Moha
- Subjects
Computer science ,Programming language ,Model transformation ,Graph theory ,computer.software_genre ,Data type ,Metamodeling ,Code refactoring ,Formal language ,Compiler ,Kermeta ,computer ,Software ,Information Systems ,computer.programming_language - Abstract
Kermeta is a meta-language for specifying the structure and behavior of graphs of interconnected objects called models. In this paper, we show that Kermeta is relatively suitable for solving three graph-based problems. First, Kermeta allows the specification of generic model transformations such as refactorings that we apply to different metamodels including Ecore, Java, and Uml. Second, we demonstrate the extensibility of Kermeta to the formal language Alloy using an inter-language model transformation. Kermeta uses Alloy to generate recommendations for completing partially specified models. Third, we show that the Kermeta compiler achieves better execution time and memory performance compared to similar graph-based approaches using a common case study. The three solutions proposed for those graph-based problems and their evaluation with Kermeta according to the criteria of genericity, extensibility, and performance are the main contribution of the paper. Another contribution is the comparison of these solutions with those proposed by other graph-based tools.
- Published
- 2010
39. Scalable shared memory LTL model checking
- Author
-
Luboš Brim, Jiří Barnat, and Petr Ročkai
- Subjects
Model checking ,Speedup ,Workflow ,Shared memory ,Computer science ,Reachability ,Distributed computing ,Scalability ,Distributed memory ,Parallel computing ,Formal verification ,Software ,Information Systems - Abstract
Recent development in computer hardware has brought more widespread emergence of shared memory, multi-core systems. These architectures offer opportunities to speed up various tasks—model checking and reachability analysis among others. In this paper, we present a design for a parallel shared memory LTL model checker that is based on a distributed memory algorithm. To improve the scalability of our tool, we have devised a number of implementation techniques which we present in this paper. We also report on a number of experiments we conducted to analyse the behaviour of our tool under different conditions using various models. We demonstrate that our tool exhibits significant speedup in comparison with sequential tools, which improves the workflow of verification in general.
- Published
- 2010
40. Model checking software: on some new waves and some evergreens
- Author
-
Dragan Bošnački, Stefan Edelkamp, Algorithms, Geometry and Applications, and Computational Biology
- Subjects
Model checking ,Programming language ,Computer science ,business.industry ,Formal equivalence checking ,Abstraction model checking ,computer.software_genre ,Partial order reduction ,Software ,Automated proof checking ,Symbolic trajectory evaluation ,Software verification and validation ,business ,computer ,Information Systems - Abstract
This paper introduces a special section of the STTT journal containing a selection of papers that were presented at the 13th International Workshop Model Checking Software SPIN 2007. We give a brief overview of the field of software model checking with emphasis on topics that are covered by the selected papers. In our focus are some emerging trends like multi-core model checking together with new high-quality model checking tools, as well as subjects that remain challenging virtually since the establishing of the discipline, like partial-order reduction and abstraction.
- Published
- 2010
41. The RE-UWA approach to recover user centered conceptual models from Web applications
- Author
-
Damiano Distante, Mario Luca Bernardi, and Giuseppe A. Di Lucca
- Subjects
Web-based simulation ,medicine.medical_specialty ,Web development ,business.industry ,Computer science ,Web engineering ,computer.software_genre ,Web design ,medicine ,Web navigation ,Mashup ,Web service ,Software engineering ,business ,computer ,Web modeling ,Software ,Information Systems - Abstract
Large-scale Web Applications, especially those intended to publish contents and provide information to its users, are by nature subject to continuous and fast changes. This often means fast obsolescence of the design documentation and a lot of effort required to comprehend the application when performing maintenance and evolution tasks. This paper presents a reverse engineering approach for Web Applications enabling the semi-automatic recovery of user-centered conceptual models describing, from a user perspective, key aspects, such as the delivered contents and navigational paths. The abstracted models are formalized according to the Ubiquitous Web Applications (UWA) design methodology, but any other design method for Web Applications could be used instead. The paper describes the recovery process, a tool developed to support the process, and the results from a case study conducted to validate the approach on a set of real world Web Applications.
- Published
- 2009
42. Special section on Web Systems Evolution
- Author
-
Filippo Ricca and Liu Chao
- Subjects
Web standards ,medicine.medical_specialty ,business.industry ,Emerging technologies ,Computer science ,Software maintenance ,Web engineering ,World Wide Web ,Web Accessibility Initiative ,medicine ,Web application ,business ,Web intelligence ,Web modeling ,Software ,Information Systems - Abstract
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.
- Published
- 2009
43. An approach and an Eclipse-based environment for enhancing the navigation structure of Web sites
- Author
-
Damiano Distante, Michele Risi, and Giuseppe Scanniello
- Subjects
Ajax ,Information retrieval ,Computer science ,Semantic analysis (machine learning) ,Semantics ,Set (abstract data type) ,Web page ,Navigability ,Cluster analysis ,computer ,Site map ,Software ,Information Systems ,computer.programming_language - Abstract
This paper presents an approach based on information retrieval and clustering techniques for automatically enhancing the navigation structure of a Web site for improving navigability. The approach increments the set of navigation links provided in each page of the site with a semantic navigation map, i.e., a set of links enabling navigating from a given page to other pages of the site showing similar or related content. The approach uses Latent Semantic Indexing to compute a dissimilarity measure between the pages of the site and a graph-theoretic clustering algorithm to group pages showing similar or related content according to the calculated dissimilarity measure. AJAX code is finally used to extend each Web page with an associated semantic navigation map. The paper also presents a prototype of a tool developed to support the approach and the results from a case study conducted to assess the validity and feasibility of the proposal.
- Published
- 2009
44. Model checking C source code for embedded systems
- Author
-
Bastian Schlich and Stefan Kowalewski
- Subjects
Model checking ,Source code ,Assembly language ,Computer science ,business.industry ,media_common.quotation_subject ,Static analysis ,Square (algebra) ,Microcontroller ,Embedded system ,Theory of computation ,Code (cryptography) ,business ,computer ,Software ,Information Systems ,media_common ,computer.programming_language - Abstract
In this paper, the applicability of model checking to C code for embedded systems is studied. The paper is divided into two parts. In the first part, 13 existing model checkers for C code are detailed and evaluated for their applicability in the verification of C code for embedded systems. A case study is presented that applied CBMC as one representative C code model checker to an exemplary microcontroller program. As a consequence of this case study, we decided to develop a new model checker for source code for microcontrollers, called [mc]square. It is described in the second part of this paper. We present the architecture and the peculiarities of [mc]square, and we successfully applied [mc]square to the same microcontroller program used in the case study.
- Published
- 2009
45. Software model checking is a rich research field
- Author
-
Antti Valmari
- Subjects
Model checking ,Distributed Computing Environment ,Theoretical computer science ,Computer science ,Programming language ,Abstraction model checking ,Symbolic execution ,computer.software_genre ,Bounded function ,Automated proof checking ,Symbolic trajectory evaluation ,Theory of computation ,computer ,Software ,Information Systems - Abstract
This introductory paper has been written for readers who know nothing about model checking but do know about software. Its aim is to present, almost without mathematical terms, the fundamental general approaches on which the papers in this Special Section build, and give an idea of what kind of contribution each paper makes. The main issues discussed are motivation for model checking, state spaces, and bounded model checking with sat solvers. Individual papers lead to discuss the following ideas: exploiting a distributed computing environment for model checking, constructing those states first that look most promising for eventually finding errors, only constructing a representative subset of states, the representation of contents of variables in an abstract way with approximation from below, and the use of more general solvers than sat solvers in bounded model checking.
- Published
- 2008
46. Special section on testing and security of Web systems
- Author
-
Alessandro Marchetto
- Subjects
Web standards ,medicine.medical_specialty ,business.industry ,Emerging technologies ,Computer science ,Web engineering ,Web application security ,Engineering management ,medicine ,Dependability ,Software engineering ,business ,Web intelligence ,Web modeling ,Software ,Information Systems ,Verification and validation - Abstract
This special section is devoted to a selection of papers that have been originally published in the Proceedings of the International Workshop on Web Quality, Verification and Validation (WQVV) held in Como, Italy, in July 2007. The workshop was part of the Seventh International Conference on Web Engineering (ICWE 2007). These papers investigate different issues of two fundamental “aspects” of quality and dependability of modern Web systems: testing and security. The main contribution of this special section consists in trying to bring the gap between research and “industrial” practice in Web systems. The use of new technologies, tools and methodologies is increasing in the Web and it makes the systems more and more interactive and responsive than in the past. Therefore, limits and problems related to specific aspects of systems quality and dependability are investigated, and new approaches and ideas are proposed to overcome such limitations.
- Published
- 2008
47. Automating test automation
- Author
-
Andrej Pietschker
- Subjects
business.industry ,Computer science ,Legacy system ,Totally integrated automation ,Automation ,Test (assessment) ,Task (project management) ,TTCN-3 ,Code (cryptography) ,Software engineering ,business ,Batch production ,Software ,Information Systems - Abstract
When trying to introduce TTCN-3 and thus improving test automation we are regularly faced with the issue of legacy test automation. These existing approaches to test automation range from small code developed for a very specific task to large applications with substantial development effort or even purchased solution from third party vendors that might include hardware components. Often these solutions cater for a specific need and their combined application is controlled by humans. A higher degree of test automation can be achieved if these solutions are combined in a test system to enable batch runs for example. TTCN-3 can be a good choice for implementing a future-oriented solution. However, recreating all of the existing parts in TTCN-3 might not be a feasible solution from a business perspective. Instead of refraining from creating an advanced solution, the idea is to use those existing parts to substantially reduce the effort necessary to introduce an improved test automation solution. In this paper, we will report on the successful integration of legacy test solutions using TTCN-3 and creating a new, advanced test system that enables overnight test runs. The paper will illustrate our challenges and experiences from this project.
- Published
- 2008
48. Coping with large design spaces: design problem solving in fluidic engineering
- Author
-
Benno Stein
- Subjects
Requirements engineering ,business.industry ,Computer science ,Computer-automated design ,Knowledge engineering ,Software development ,User requirements document ,Case-based reasoning ,Electronic design automation ,Probabilistic design ,Artificial intelligence ,business ,Software engineering ,Software ,Information Systems - Abstract
This paper is about tool support for knowledge-intensive engineering tasks. In particular, it introduces software technology to assist the design of complex technical systems. There is a long tradition in automated design problem solving in the field of artificial intelligence, where, especially in the early stages, the search paradigm dictated many approaches. Later, in the so-called modern period, a better problem understanding led to the development of more adequate problem solving techniques. However, search still constitutes an indispensable part in computer-based design problem solving—albeit many human problem solvers get by without (almost). We tried to learn lessons from this observation, and one is presented in this paper. We introduce design problem solving by functional abstraction which follows the motto: construct a poor solution with little search, which then must be repaired. For the domain of fluidic engineering we have operationalized the paradigm by the combination of several high-level techniques. The red thread of this paper is design automation, but the presented technology does also contribute in the following respects: (a) productivity enhancement by relieving experts from auxiliary and routine tasks; (b) formulation, exchange, and documentation of knowledge about design; (c) requirements engineering, feasibility analysis, and validation.
- Published
- 2008
49. Model based development of access policies
- Author
-
Muhammad Alam, Gerhard Popp, and Ruth Breu
- Subjects
Object-oriented programming ,Programming language ,business.industry ,Computer science ,Access control ,Context (language use) ,Permission ,computer.software_genre ,Object (computer science) ,First-order logic ,Algebraic semantics ,Model-based design ,Artificial intelligence ,business ,computer ,Software ,Information Systems - Abstract
In this paper we present a novel approach for the specification of user rights in the context of an object oriented use case driven development process. Basically, we extend the specification of methods by a permission section describing the right of some actor to call the method of an object. Our approach is both role based and context based while allowing for permissions to be specified at a fine-grained data-dependent level. We use first-order logic with a built-in notion of objects and classes (provided with an algebraic semantics) as our syntactic and semantic framework. In the second part of the paper, we demonstrate the application of this approach in a model-based context to generate permissions in distributed peer-to-peer networks.
- Published
- 2007
50. Slicing concurrent Java programs using Indus and Kaveri
- Author
-
John Hatcliff and Venkatesh-Prasad Ranganath
- Subjects
Object-oriented programming ,Java ,Computer science ,Programming language ,media_common.quotation_subject ,Program comprehension ,Program transformation ,computer.software_genre ,Slicing ,Program analysis ,Debugging ,Program slicing ,computer ,Software ,Information Systems ,media_common ,computer.programming_language - Abstract
Program slicing is a program analysis and transformation technique that has been successfully used in a wide range of applications including program comprehension, debugging, maintenance, testing, and verification. However, there are only few fully featured implementations of program slicing that are available for industrial applications or academic research. In particular, very little tool support exists for slicing programs written in modern object-oriented languages such as Java, C#, or C++. In this paper, we present Indus—a robust framework for analyzing and slicing concurrent Java programs, and Kaveri—a feature-rich Eclipse-based GUI front end for Indus slicing. For Indus, we describe the underlying tool architecture, analysis components, and program dependence capabilities required for slicing. In addition, we present a collection of advanced features useful for effective slicing of Java programs including calling-context sensitive slicing, scoped slicing, control slicing, and chopping. For Kaveri, we discuss the design goals and basic capabilities of the graphical facilities integrated into a Java development environment to present the slicing information. This paper is an extended version of a tool demonstration paper presented at the International Conference on Fundamental Aspects of Software Engineering (FASE 2005). Thus, the paper highlights tool capabilities and engineering issues and refers the reader to other papers for technical details.
- Published
- 2007
Discovery Service for Jio Institute Digital Library
For full access to our library's resources, please sign in.