Search results for "Model-Checking"
showing 7 items of 7 documents
RDF2SPIN: Mapping Semantic Graphs to SPIN Model Checker
2011
International audience; The most frequently used language to represent the semantic graphs is the RDF (W3C standard for meta-modeling). The construction of semantic graphs is a source of numerous errors of interpretation. The processing of large semantic graphs is a limit to the use of semantics in current information systems. The work presented in this paper is part of a new research at the border between two areas: the semantic web and the model checking. For this, we developed a tool, RDF2SPIN, which converts RDF graphs into SPIN language. This conversion aims checking the semantic graphs with the model checker SPIN in order to verify the consistency of the data. To illustrate our propos…
RDF2NμSMV: Mapping Semantic Graphs to NμSMV Model Checker
2011
International audience; The most frequently used language to represent the semantic graphs is the RDF (W3C standard for meta-modeling). The construction of semantic graphs is a source of numerous errors of interpretation. The processing of large semantic graphs is a limit to the use of semantics in current information systems. The work presented in this paper is part of a new research at the border between two areas: the Semantic Web and the model checking. For this, we developed a tool, RDF2NμSMV, which converts RDF graphs into NμSMV language. This conversion aims checking the semantic graphs with the model checker NμSMV in order to verify the consistency of the data. To illustrate our pro…
Qualifying semantic graphs using model checking
2011
International audience; Semantic interoperability problems have found their solutions using languages and techniques from the Semantic Web. The proliferation of ontologies and meta-information has improved the understanding of information and the relevance of search engine responses. However, the construction of semantic graphs is a source of numerous errors of interpretation or modeling and scalability remains a major problem. The processing of large semantic graphs is a limit to the use of semantics in current information systems. The work presented in this paper is part of a new research at the border of two areas: the semantic web and the model checking. This line of research concerns t…
Sequentializing Parameterized Programs
2012
We exhibit assertion-preserving (reachability preserving) transformations from parameterized concurrent shared-memory programs, under a k-round scheduling of processes, to sequential programs. The salient feature of the sequential program is that it tracks the local variables of only one thread at any point, and uses only O(k) copies of shared variables (it does not use extra counters, not even one counter to keep track of the number of threads). Sequentialization is achieved using the concept of a linear interface that captures the effect an unbounded block of processes have on the shared state in a k-round schedule. Our transformation utilizes linear interfaces to sequentialize the progra…
Formal verification of a Cooperative Automatic Repeat reQuest MAC protocol
2012
Author's version of an article published in the journal: Computer Standards & Interfaces. Also available from the publisher at: http://dx.doi.org/10.1016/j.csi.2011.12.001 Cooperative communications, in which a relay node helps the source node to deliver its packets to the destination node, are able to obtain significant benefits in terms of transmission reliability, coverage extension and energy efficiency. A Cooperative Automatic Repeat reQuest (C-ARQ) MAC protocol has been recently proposed to exploit cooperative diversity at the MAC layer. in this paper, we validate the integrity and the validity of the C-ARQ protocol using formal methods. The protocol logic is modeled in SDL and implem…
SCALESEM : Evaluation of Semantic Graph based on Model Checking
2011
International audience; Semantic interoperability problems have found their solutions using languages and techniques from the Semantic Web. The proliferation of ontologies and meta-information has improved the understanding of information and the relevance of search engine responses. However, the construction of semantic graphs is a source of numerous errors of interpretation or modelling and scalability remains a major problem. The processing of large semantic graphs is a limit to the use of semantics in current information systems. The work presented in this paper is part of a new research at the border of two areas: the semantic web and the model checking. This line of research concerns …
Modular Strategies for Recursive Game Graphs
2006
AbstractMany problems in formal verification and program analysis can be formalized as computing winning strategies for two-player games on graphs. In this paper, we focus on solving games in recursive game graphs which can model the control flow in sequential programs with recursive procedure calls. While such games can be viewed as the pushdown games studied in the literature, the natural notion of winning in our framework requires the strategies to be modular with only local memory; that is, resolution of choices within a module does not depend on the context in which the module is invoked, but only on the history within the current invocation of the module. While reachability in (global…