We present Comparator, a tool that measures the compatibility between two behavioural interfaces. Comparator can be used as a stand-alone Web application, and is also integrated into a model-based adaptation toolbox.
ISBN:
(纸本)9783642548048;9783642548031
We present Comparator, a tool that measures the compatibility between two behavioural interfaces. Comparator can be used as a stand-alone Web application, and is also integrated into a model-based adaptation toolbox.
the paper extends single-pushout graph transformation by polymorphism, a key concept in object-oriented design. the notions sub-rule and remainder, well-known in single-pushout rewriting, are applied in order to model...
详细信息
ISBN:
(纸本)9783642548048;9783642548031
the paper extends single-pushout graph transformation by polymorphism, a key concept in object-oriented design. the notions sub-rule and remainder, well-known in single-pushout rewriting, are applied in order to model dynamic rule extension and type dependent rule application. this extension mechanism qualifies graph transformation as a modelling technique for extendable frameworks. therefore, it contributes to the applicability of graph transformation in software engineering.
We study models of software systems with variants that stem from a specific choice of configuration parameters with a direct impact on performance properties. Using UML activity diagrams with quantitative annotations,...
详细信息
ISBN:
(纸本)9783642548048;9783642548031
We study models of software systems with variants that stem from a specific choice of configuration parameters with a direct impact on performance properties. Using UML activity diagrams with quantitative annotations, we model such systems as a product line. the efficiency of a product-based evaluation is typically low because each product must be analyzed in isolation, making difficult the re-use of computations across variants. Here, we propose a family-based approach based on symbolic computation. A numerical assessment on large activity diagrams shows that this approach can be up to three orders of magnitude faster than product-based analysis in large models, thus enabling computationally efficient explorations of large parameter spaces.
Copying, or cloning, is a basic operation used in the specification of many applications in computer science. However, when dealing with complex structures, like graphs, cloning is not a straightforward operation sinc...
详细信息
ISBN:
(纸本)9783642548048;9783642548031
Copying, or cloning, is a basic operation used in the specification of many applications in computer science. However, when dealing with complex structures, like graphs, cloning is not a straightforward operation since a copy of a single vertex may involve (implicitly) copying many edges. therefore, most graph transformation approaches forbid the possibility of cloning. We tackle this problem by providing a framework for graph transformations with cloning. We use attributed graphs and allow rules to change attributes. these two features (cloning/changing attributes) together give rise to a powerful formal specification approach. In order to handle different kinds of graphs and attributes, we first define the notion of attributed structures in an abstract way. then we generalise the sesqui-pushout approach of graph transformation in the proposed general framework and give appropriate conditions under which attributed structures can be transformed. Finally, we instantiate our general framework with different examples, showing that many structures can be handled and that the proposed framework allows one to specify complex operations in a natural way.
While most debugging techniques focus on patching implementations, there are bugs whose most appropriate corrections consist in fixing the specification to prevent invalid executions-such as to define the correct inpu...
详细信息
ISBN:
(纸本)9783642548048;9783642548031
While most debugging techniques focus on patching implementations, there are bugs whose most appropriate corrections consist in fixing the specification to prevent invalid executions-such as to define the correct input domain of a function. In this paper, we present a fully automatic technique that fixes bugs by proposing changes to contracts (simple executable specification elements such as pre- and postconditions). the technique relies on dynamic analysis to understand the source of buggy behavior, to infer changes to the contracts that emend the bugs, and to validate the changes against general usage. We have implemented the technique in a tool called SpeciFix, which works on programs written in Eiffel, and evaluated it on 44 bugs found in standard data-structure libraries. Manual analysis by human programmers found that SpeciFix suggested repairs that are deployable for 25% of the faults;in most cases, these contract repairs were preferred over fixes for the same bugs that change the implementation.
Security has become the Achilles' heel of most modern software systems. Techniques ranging from the manual inspection to automated static and dynamic analyses are commonly employed to identify security vulnerabili...
详细信息
ISBN:
(纸本)9783642548048;9783642548031
Security has become the Achilles' heel of most modern software systems. Techniques ranging from the manual inspection to automated static and dynamic analyses are commonly employed to identify security vulnerabilities prior to the release of the software. However, these techniques are time consuming and cannot keep up withthe complexity of ever-growing software repositories (e.g., Google Play and Apple App Store). In this paper, we aim to improve the status quo and increase the efficiency of static analysis by mining relevant information from vulnerabilities found in the categorized software repositories. the approach relies on the fact that many modern software systems are developed using rich application development frameworks (ADF), allowing us to raise the level of abstraction for detecting vulnerabilities and thereby making it possible to classify the types of vulnerabilities that are encountered in a given category of application. We used open-source software repositories comprising more than 7 million lines of code to demonstrate how our approach can improve the efficiency of static analysis, and in turn, vulnerability detection.
Model finders are becoming useful in many software engineering problems. Kodkod [19] is one of the most popular, due to its support for relational logic (a combination of first order logic with relational algebra oper...
详细信息
ISBN:
(纸本)9783642548048;9783642548031
Model finders are becoming useful in many software engineering problems. Kodkod [19] is one of the most popular, due to its support for relational logic (a combination of first order logic with relational algebra operators and transitive closure), allowing a simpler specification of constraints, and support for partial instances, allowing the specification of a priori (exact, but potentially partial) knowledge about a problem's solution. However, in some software engineering problems, such as model repair or bidirectional model transformation, knowledge about the solution is not exact, but instead there is a known target that the solution should approximate. In this paper we extend Kodkod's partial instances to allow the specification of such targets, and show how its model finding procedure can be adapted to support them (using both PMax-SAT solvers or SAT solvers with cardinality constraints). Two case studies are also presented, including a careful performance evaluation to assess the effectiveness of the proposed extension.
the automated analysis and verification of pointer-manipulating programs operating on a heap is a challenging task. It requires abstraction techniques for dealing with complex program behaviour and unbounded state spa...
详细信息
ISBN:
(纸本)9783319091082;9783319091075
the automated analysis and verification of pointer-manipulating programs operating on a heap is a challenging task. It requires abstraction techniques for dealing with complex program behaviour and unbounded state spaces that arise from both dynamic data structures and recursive procedures. In previous work it was shown that hyperedge replacement grammars provide an intuitive and versatile concept for defining and implementing such abstractions. Here we extend this approach towards a modular way of reasoning about programs with (possibly recursive) procedures featuring local variables. We propose an interprocedural dataflow analysis to automatically derive procedure contracts, i.e., graph transformations that concisely capture the overall effect of a procedure. Besides its modularity, another advantage of this analysis is that it relieves us from explicitly modelling the call stack on the heap, i.e., heap and control abstraction are clearly separated. the former can now be specified by simple and intuitive hyperedge replacement grammars describing the data structures only, while the latter is realised by automatically generated procedure contracts.
We present a formal verification approach for detecting design issues related to user interaction, with a focus on user interface of medical devices. the approach makes a novel use of configuration diagrams proposed b...
详细信息
ISBN:
(纸本)9783642548048;9783642548031
We present a formal verification approach for detecting design issues related to user interaction, with a focus on user interface of medical devices. the approach makes a novel use of configuration diagrams proposed by Rushby to formally verify important human factors properties of user interface implementation. In particular, it first translates the software implementation of user interface into an equivalent formal specification, from which a behavioral model is constructed using theorem proving;human factors properties are then verified against the behavioral model;lastly, a comprehensive set of test inputs are produced by exploring the behavioral model, which can be used to challenge the real interface implementation and to ensure that the issues detected in the behavior model do apply to the implementation. We have prototyped the approach based on the PVS proof system, and applied it to analyze the user interface of a real medical device. the analysis detected several interaction design issues in the device, which may potentially lead to severe consequences.
We consider computation in the presence of closed timelike curves (CTCs), as proposed by Deutsch. We focus on the case in which the CTCs carry classical bits (as opposed to qubits). Previously, Aaronson and Watrous sh...
详细信息
ISBN:
(纸本)9783939897774
We consider computation in the presence of closed timelike curves (CTCs), as proposed by Deutsch. We focus on the case in which the CTCs carry classical bits (as opposed to qubits). Previously, Aaronson and Watrous showed that computation with polynomially many CTC bits is equivalent in power to PSPACE. On the other hand, Say and Yakaryilmaz showed that computation with just 1 classical CTC bit gives the power of "postselection", thereby upgrading classical randomized computation (BPP) to the complexity class BPPpath and standard quantum computation (BQP) to the complexity class PP. It is natural to ask whether increasing the number of CTC bits from 1 to 2 (or 3, 4, etc.) leads to increased computational power. We show that the answer is no: randomized computation with logarithmically many CTC bits (i.e., polynomially many CTC states) is equivalent to BPPpath. (Similarly, quantum computation augmented with logarithmically many classical CTC bits is equivalent to PP.) Spoilsports with no interest in time travel may view our results as concerning the robustness of the class BPPpath and the computational complexity of sampling from an implicitly defined Markov chain.
暂无评论