Advanced tools used in model-based systems engineering (MBSE) frequently represent their models as graphs. In order to test those tools, the automated generation of well-formed (or intentionally malformed) graph model...
详细信息
Advanced tools used in model-based systems engineering (MBSE) frequently represent their models as graphs. In order to test those tools, the automated generation of well-formed (or intentionally malformed) graph models is necessitated which is often carried out by solver-based model generation techniques. In many model generation scenarios, one needs more refined control over the generated unit tests to focus on the more relevant models. Type scopes allow to precisely define the required number of newly generated elements, thus one can avoid the generation of unrealistic and highly symmetric models having only a single type of elements. In this paper, we propose a 3-valued scoped partial modeling formalism, which innovatively extends partial graph models with predicate abstraction and counter abstraction. As a result, well-formedness constraints and multiplicity requirements can be evaluated in an approximated way on incomplete (unfinished) models by using advanced graph query engines with numerical solvers (e.g., IP or LP solvers). Based on the refinement of 3-valued scoped partial models, we propose an efficient model generation algorithm that generates models that are both well-formed and satisfy the scope requirements. We show that the proposed approach scales significantly better than existing SAT-solver techniques or the original graph solver without multiplicity reasoning. We illustrate our approach in a complex design-space exploration case study of collaborating satellites introduced by researchers at NASA JPL.
Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers, this means being able to have releva...
详细信息
Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers, this means being able to have relevant properties, such as modes, types, determinacy, nonfailure, sharing, constraints, and cost, checked and errors flagged without having to actually run the program. Such global static analysis tools are arguably most useful the earlier they are used in the software development cycle, and fast response times are essential for interactive use. Triggering a full and precise semantic analysis of a software project every time a change is made can be prohibitively expensive. This is specially the case when complex properties need to be inferred for large, realistic code bases. In our static analysis and verification framework, this challenge is addressed through a combination of modular and incremental (context- and path-sensitive) analysis that is responsive to program edits, at different levels of granularity. In this tool paper, we present how the combination of this framework within an integrated development environment (IDE) takes advantage of such incrementality to achieve a high level of reactivity when reflecting analysis and verification results back as colorings and tooltips directly on the program text - the tool's VeriFly mode. The concrete implementation that we describe is Emacs-based and reuses in part off-the- shelf "on-the-fly" syntax checking facilities (flycheck). We believe that similar extensions are also reproducible with low effort in other mature development environments. Our initial experience with the tool shows quite promising results, with low latency times that provide early, continuous, and precise assertion checking and other semantic feedback to programmers during the development process. The tool supports Prolog natively, as well as other languages by semantic transformation into Horn clauses.
Context-sensitive global analysis of large code bases can be expensive, which can make its use impractical during software development. However, there are many situations in which modifications are small and isolated ...
详细信息
Context-sensitive global analysis of large code bases can be expensive, which can make its use impractical during software development. However, there are many situations in which modifications are small and isolated within a few components, and it is desirable to reuse as much as possible previous analysis results. This has been achieved to date through incremental global analysis fixpoint algorithms that achieve cost reductions at fine levels of granularity, such as changes in program lines. However, these fine-grained techniques are neither directly applicable to modular programs nor are they designed to take advantage of modular structures. This paper describes, implements, and evaluates an algorithm that performs efficient context-sensitive analysis incrementally on modular partitions of programs. The experimental results show that the proposed modular algorithm shows significant improvements, in both time and memory consumption, when compared to existing non-modular, fine-grain incremental analysis techniques. Furthermore, thanks to the proposed intermodular propagation of analysis information, our algorithm also outperforms traditional modular analysis even when analyzing from scratch.
We investigate in this work a generalization of the known CNF representation which allows an efficient Boolean encoding for n-ary CSPs. We show that the space complexity of the Boolean encoding is identical to the one...
详细信息
ISBN:
(纸本)3540409300
We investigate in this work a generalization of the known CNF representation which allows an efficient Boolean encoding for n-ary CSPs. We show that the space complexity of the Boolean encoding is identical to the one of the classical CSP representation and introduce a new inference rule whose application until saturation achieves arc-consistency in a linear time complexity for n-ary CSPs expressed in the Boolean encoding. Two enumerative methods for the Boolean encoding are studied: the first one (equivalent to MAC in CSPs) maintains full arc-consistency on each node of the search tree while the second (equivalent to FC in CSPs) performs partial arc-consistency on each node. Both methods are experimented and compared on some instances of the Ramsey problem and randomly generated 3-ary CSPs and promising results are obtained.
We introduce the most recent and advanced implementation of constraint handling rules (CHR) in a logicprogramming language, which improves both on previous implementations (in terms of completeness, flexibility and e...
详细信息
ISBN:
(数字)9783540481645
ISBN:
(纸本)3540665404
We introduce the most recent and advanced implementation of constraint handling rules (CHR) in a logicprogramming language, which improves both on previous implementations (in terms of completeness, flexibility and efficiency) and on the principles that should guide such a Prolog implementation consisting of a runtime system and a compiler. The runtime system utilizes attributed variables for the realization of the constraint store with efficient retrieval and update mechanisms. Rules describing the interactions between constraints are compiled into Prolog clauses by a multi-phase compiler, the core of which comprises a small number of compact code generating templates in the form of definite clause grammar rules.
暂无评论