Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Verification of Graph-based Model Transformations Using Alloy
Get PDFModel transformations are fundamental in model driven development. Thus, verification of model transformations is indispensable to ensure the quality and the reliability of transformation results. In this paper we focus on graph-based model transformation systems using the double-pushout (DPO) approach and study their correctness w.r.t. conformance. It means that, given a transformation system and a valid source model, any applicable sequences of model transformations will produce a valid target model.A procedure is presented to verify firstly if a model transformation system is correct w.r.t. conformance by checking the Direct Condition, i.e., each direct model transformation produces a valid target model from a valid source model. Then, for systems not satisfying the direct condition, it checks theSequential Condition, i.e., if a direct model transformation t produces an invalid target model from a valid source model, then there exists a sequence of direct model transformations succeeding the transformation tthat produces a valid target model. The satisfiability of the latter condition cannot always promise correctness, but it ensures that, from every valid source model, a valid target model can be produced. The procedure uses a bounded verification approach based on First Order Logic (FOL). The approach encodes a transformation system and the two conditions into a relational logic specification in Alloy. Then the specification is inspected by the Alloy Analyzer to check if the system satisfies the conditions. When it violates the conditions, the analyzer presents a counterexample, that may be used to redesign the system. An example is given to illustrate the bounded verification approach in the Diagram Predicate Framework (DPF)
PVSio-web: a tool for rapid prototyping device user interfaces in PVS
Get PDFWe present PVSio-web which extends the simulation component of the PVS proof system with functionalities for rapid prototyping device user interfaces. The tool presents itself as a classic image-editing environment with functionalities such as area selection and hyperlink creation, thus reducing the barriers that prevent non-experts in formal methods from using PVS. Designers load a picture of the layout of the device user interface under development, specify interactive areas over the layout, and link them to a PVS specification. They can then explore the behaviour of the formal user interface specification through point-and-click interactions. The architecture of the tool is general, and can be used as the basis for extending other verification tools. A demonstration of the capabilities of PVSio-web is presented through an example based on a commercial medical device user interface. Our ultimate aim is to promote and facilitate the use of formal verification tools when developing device user interfaces
13th International Workshop on Graph Transformation and Visual Modeling Techniques (GTVMT 2014): Preface
Get PDFAutomatic Proving of Fuzzy Formulae with Fuzzy Logic Programming and SMT
Get PDFIn this paper we deal with propositional fuzzy formulae containing severalpropositional symbols linked with connectives defined in a lattice of truth degrees more complex than Bool. We firstly recall an SMT (Satisfiability Modulo Theories) based method for automatically proving theorems in relevant infinitely valued (including Łukasiewicz and G¨odel) logics. Next, instead of focusing on satisfiability (i.e., proving the existence of at least one model) or unsatisfiability, our interest moves to the problem of finding the whole set of models (with a finite domain) for a given fuzzy formula. We propose an alternative method based on fuzzy logic programming where the formula is conceived as a goal whose derivation tree contains on its leaves all the models of the original formula, by exhaustively interpreting each propositional symbol in all the possible forms according the whole setof values collected on the underlying lattice of truth-degrees
Robust Parsing of Cloned Token Sequences
Get PDFToken-based clone detection techniques are known for theirscalability, high recall, and robustness against syntax errors andincomplete code. They, however, may yield clones that aresyntactically incomplete and they know very little about the syntacticstructure of their reported clones. Hence, their results cannotimmediately be used for automated refactorings or syntactic filtersfor relevance.This paper explores techniques of robust parsing to parse codefragments reported by token-based clone detectors to determine whetherthe clones are syntactically complete and what kind of syntacticelements they contain.This knowledge can be used to improve the precision of token-basedclone detection
R-SQL: An SQL Database System with Extended Recursion
Get PDFThe relational database language SQL:1999 standard supports recursion, but this approach is limited to the linear case. Moreover, mutual recursion is not supported, and negation cannot be combined with recursion. We designed the language R-SQL to overcome these limitations, improving termination properties in recursive definitions. In addition we developed a proof of concept implementation of an R-SQL system. In this paper we describe in detail an improved system enhancing performance. It can be integrated into existing RDBMS's, extending them with the aforementioned benefits of R-SQL. The system processes an R-SQL database definition obtaining its extension in tables of an RDBMS (such as PostgreSQL and DB2). It is implemented in SWI-Prolog and it produces a Python script that, upon execution, computes the result of the R-SQL relations. We provide some performance results showing the efficiency gains w.r.t. the previous version. We also include a comparative analysis including some representative relational a deductive systems
A Formal Co-Simulation Approach for Wireless Sensor Network Development
Get PDFThis paper proposes a Formal Co-simulation (FoCoSim-WSN) framework to provide a good software engineering practice for wireless sensor networks (WSNs) including high-level abstraction, separation of concerns, strong verification and validation (V&V) techniques. This provides an iterative interworking framework which combines the benefits of existing simulation and proof-based formal verification approaches. The complexity of software development for the sensor node controller is reduced by separating the controller model from the simulation environment. Controller algorithms from application through network and MAC layers can be formally developed and verified in a layered manner using the refinement method of the Event-B language and its RODIN toolkit. The absence of certain classes of faults in controller models which cannot be guaranteed by simulation testing techniques, can be proved by formal methods. On the other hand, the MiXiM simulation of physical environment provides full confidence about reliability and performance analysis through long running simulation via wireless channels. Our prototype development confirms the flexibility of the framework for interworking between formal, simulation and co-simulation modelling
A Model-Based Approach to Impact Analysis Using Model Differencing
Get PDFImpact analysis is concerned with the identification of consequences of changes and is therefore an importantactivity for software evolution. In model-based software development, models are core artifacts,which are often used to generate essential parts of a software system.Changes to a model can thus substantially affect different artifacts of a softwaresystem. In this paper, we propose a model-based approach to impact analysis, in whichexplicit impact rules can be specified in a domain specific language (DSL). These impact rules define consequences of designated UML classdiagram changes on software artifacts and the need of dependent activitiessuch as data evolution. The UML class diagram changes are identified automaticallyusing model differencing. The advantage of using explicit impact rules is thatthey enable the formalization of knowledge about a product.By explicitly defining this knowledge, it is possible to create a checklistwith hints about development steps that are (potentially) necessary to managethe evolution. To validate the feasibility of our approach, we provide resultsof a case study
Functional and Performance Analysis of Network-on-Chips Using Actor-based Modeling and Formal Verification
Get PDFNetwork on Chip (NoC) has emerged as a promising architecture paradigmfor todays many-core systems. As complexity grows in NoCs, functional verificationand performance prediction in the early stages of the design process are suggestedas ways to reduce the fabrication cost. Formal methods have gained moreattention as alternative ways for analyzing NoC designs. In this paper we propose amethod to model different characteristics of the system, and also verify various functionaland performance properties by generating the full state space of the model fordifferent scenarios. We present a formal model for two-dimensional mesh GloballyAsynchronous Locally Synchronous (GALS) NoCs with four-phase handshakecommunication protocol, using the actor-based modeling language Rebeca. Functionaland timing behaviors, routing algorithm and communication protocol are capturedin the model. Deadlock freedom, message arrival, and end-to-end packet latencyare checked. In order to analyze large NoCs we propose a scalable approachbased on compositional verification for estimating maximum end-to-end packet latency.The compositional approach is specific for the XY-routing algorithm. Resultsof verification are compared and matched to simulation results of HSPICE using32nm technology