1,721,338 research outputs found
Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, October 10-12, 2018, Proceedings.
No full text[No abstract available]11Nscopu
Model checking linear temporal logic of rewriting formulas under localized fairness
No full textThis paper presents the linear temporal logic of rewriting (LTLR) model checker under localized fairness assumptions for the Maude system. The linear temporal logic of rewriting extends linear temporal logic (LTL) with spatial action patterns that describe patterns of rewriting events. Since LTLR generalizes and extends various state-based and event-based logics, mixed properties involving both state propositions and actions, such as fairness properties, can be naturally expressed in LTLR. However, often the needed fairness assumptions cannot even be expressed as propositional temporal logic formulas because they are parametric, that is, they correspond to universally quantified temporal logic formulas. Such universal quantification is succinctly captured by the notion of localized fairness; for example, fairness is localized to the object name parameter in object fairness conditions. We summarize the foundations, and present the language design and implementation of the Maude Fair LTLR model checker, developed at the C++ level within the Maude system by extending the existing Maude LTL model checker. Our tool provides not only an efficient LTLR model checking algorithm under parameterized fairness assumptions but also suitable specification languages as part of its user interface. The expressiveness and effectiveness of the Maude Fair LTLR model checker are illustrated by five case studies. This is the first tool we are aware of that can model check temporal logic properties under parameterized fairness assumptions. (C) 2014 Elsevier B.V. All rights reserved.11910sciescopu
Hybrid Multirate PALS
No full textMultirate PALS reduces the design and verification of a virtually synchronous distributed real-time system to the design and verification of the underlying synchronous model. This paper introduces Hybrid Multirate PALS, which extends Multirate PALS to virtually synchronous distributed multirate hybrid systems, such as aircraft and power plant control systems. Such a system may have interrelated local physical environments, each of whose continuous behaviors may periodically change due to actuator commands. We define continuous interrelated local physical environments, and the synchronous and asynchronous Hybrid Multirate PALS models, and give a trace equivalence result relating a synchronous and an asynchronous model. Finally, we illustrate by an example how invariants can be verified using SMT solving.110Nsciescopu
Autonomous clustering scheme for wireless sensor networks using coverage estimation-based self-pruning
No full textEnergy-efficient operations are essential to prolonging the lifetime of wireless sensor networks. Clustering sensor nodes is one approach that can reduce energy consumption by aggregating data, controlling transmission power levels, and putting redundant sensor nodes to sleep. To distribute the role of a cluster head, clustering approaches should be based on efficient cluster configuration schemes. Therefore, low overhead in the cluster configuration process is one of the key constraints for energy-efficient clustering. In this paper, we present an autonomous clustering approach using a coverage estimation-based self-pruning algorithm. Our strategy for clustering is to allow the best candidate node within its own cluster range to declare itself as a cluster head and to dominate the other nodes in the range. This same self-declaration strategy is also used in the active sensor election process. As a result, the proposed scheme can minimize clustering overheads by obviating both the requirements of collecting neighbor information beforehand and the iterative negotiating steps of electing cluster heads. The proposed scheme allows any type of sensor network application, including spatial query execution or periodic environment monitoring, to operate in an energy-efficient manner
Formal patterns for multirate distributed real-time systems
No full textDistributed real-time systems (DRTSs), such as avionics and automotive systems, are very hard to design and verify. Besides the difficulties of asynchrony, clock skews, and network delays, an additional source of complexity comes from the multirate nature of many such systems, which must implement several levels of hierarchical control at different rates. In previous work we showed how the design and implementation of a single-rate DRTS which should behave in a virtually synchronous way can be drastically simplified by the PALS model transformation that generates the DRTS from a much simpler synchronous model. In this work we present several simple model transformations and a multirate extension of the PALS pattern which can be combined to reduce the design and verification of a virtually synchronous multirate DRTS to the much simpler task of specifying and verifying a single synchronous system. We illustrate the ideas with a multirate hierarchical control system where a central controller orchestrates control systems in the ailerons and tail of an airplane to perform turning maneuvers. (C) 2013 Elsevier B.V. All rights reserved.1156sciescopu
Symbolic state space reduction with guarded terms for rewriting modulo SMT
No full textRewriting modulo SMT is a novel symbolic technique to model and analyze infinite-state systems that interact with a non-deterministic environment, by seamlessly combining rewriting modulo equational theories, SMT solving, and model checking. This paper presents guarded terms, an approach to deal with the symbolic state-space explosion problem for rewriting modulo SMT, one of the main challenges of this technique. Guarded terms can encode many symbolic states into one by using SMT constraints as part of the term structure. This approach enables the reduction of the symbolic state space by limiting branching due to concurrent computation, and the complexity and size of constraints by distributing them in the term structure. A case study of an unbounded and symbolic priority queue illustrates the approach. (C) 2019 Elsevier B.V. All rights reserved.11Nsciescopu
Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude
No full textThis paper defines a real-time rewriting logic semantics for a significant subset of Ptolemy II discrete-event models. This is a challenging task, since such models combine a synchronous fixed-point semantics with hierarchical structure, explicit time, and a rich expression language. The code generation features of Ptolemy II have been leveraged to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model, and to integrate Real-Time Maude verification of the synthesized model into Ptolemy II. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude. We illustrate such formal verification of Ptolemy II models with three case studies. (C) 2010 Elsevier B.V. All rights reserved.111016sciescopu
- …
