scholarly journals SMT for state-based formal methods: the ASM case study

10.29007/djdz ◽  
2018 ◽  
Author(s):  
Paolo Arcaini ◽  
Angelo Gargantini ◽  
Elvinia Riccobene
Keyword(s):  
Computational Model ◽  
Symbolic Representation ◽  
Transition System ◽  
Explicit Representation ◽  
State Machines ◽  
Transition Systems ◽  
Smt Solver ◽  
Finite State ◽  
Satisfiability Checking

State-based transition systems can take advantage of a symbolic representation of the concepts of state and transition in order to automatically solve verification questions that could not be otherwise tackled in terms of explicit representation of the transition system. We report here our experience in developing solutions, approaches and supporting tools of verification problems regarding the Abstract State Machines (ASMs), a transition system which can be considered as an extension of Finite State Machines. We present the symbolic representation of an ASM and of its computational model in terms of the Yices SMT solver. We also discuss two scenarios of verification questions regarding the ASMs for which the symbolic representation helped us to formalize and solve the problem by satisfiability checking, namely automatic proof of correct ASM refinement and runtime verification.

scholarly journals A DESIGN FOR VERIFICATION APPROACH USING AN EMBEDDING OF PSL IN AsmL

2007 ◽  
Vol 16 (06) ◽  
pp. 859-881 ◽  
Author(s):  
AMJAD GAWANMEH ◽  
SOFIÈNE TAHAR ◽  
HAJA MOINUDEEN ◽  
ALI HABIBI
Keyword(s):  
Model Checking ◽  
Design Process ◽  
Finite State Machine ◽  
System Level ◽  
State Machines ◽  
Top Down ◽  
Finite State ◽  
Property Specification ◽  
Large Systems

In this paper, we propose to integrate an embedding of Property Specification Language (PSL) in Abstract State Machines Language (AsmL) with a top–down design for verification approach in order to enable the model checking of large systems at the early stages of the design process. We provide a complete embedding of PSL in the ASM language AsmL, which allows us to integrate PSL properties as a part of the design. For verification, we propose a technique based on the AsmL tool that translates the code containing both the design and the properties into a finite state machine (FSM) representation. We use the generated FSM to run model checking on an external tool, here SMV. Our approach takes advantage of the AsmL language capabilities to model designs at the system level as well as from the power of the AsmL tool in generating both C# code and FSMs from AsmL models. We applied our approach on the PCI-X bus standard, which AsmL model was constructed from the informal standard specifications and a subsequent UML model. Experimental results on the PCI-X bus case study showed a superiority of our approach to conventional verification.

scholarly journals Multitiered Nonlinear Morphology Using Multitape Finite Automata: A Case Study on Syriac and Arabic

2000 ◽  
Vol 26 (1) ◽  
pp. 77-105 ◽  
Author(s):  
George Anton Kiraz
Keyword(s):  
Finite Automata ◽  
State Machines ◽  
Surface Form ◽  
Lexical Representations ◽  
Tier Ii ◽  
Autosegmental Phonology ◽  
Finite State ◽  
Rewrite Rules ◽  
Main Components

This paper presents a computational model for nonlinear morphology with illustrations from Syriac and Arabic. The model is a multitiered one in that it allows for multiple lexical representations corresponding to the multiple tiers of autosegmental phonology. The model consists of three main components: (i) a lexicon, which is made of sublexica, with each sublexicon representing lexical material from a specific tier, (ii) a rewrite rules component that maps multiple lexical representations into one surface form and vice versa, and (iii) a morphotactic component that employs regular grammars. The system is finite-state in that lexica and rules can be represented by multitape finite-state machines.

scholarly journals On the Modeling of Sequential Reactive Systems by Means of Real Time Automata

2020 ◽  
Vol 27 (4) ◽  
pp. 396-411
Author(s):  
Evgeney Maximovich Vinarskii ◽  
Vladimir Anatolyevich Zakharov
Keyword(s):  
Real Time ◽  
Reactive Systems ◽  
Finite State Machines ◽  
Reactive System ◽  
State Machines ◽  
Time Model ◽  
Transition Systems ◽  
Input Signals ◽  
Finite State ◽  
Definition Of

Sequential reactive systems include hardware devices and software programs which operate in continuous interaction with the external environment, from which they receive streams of input signals (data, commands) and in response to them form streams of output signals. Systems of this type include controllers, network switches, program interpreters, system drivers. The behavior of some reactive systems is determined not only by the sequence of values of input signals, but also by the time of their arrival at the inputs of the system and the delays in computing the output signals. These aspects of reactive system computations are taken into account by real-time models of computation which include, in particular, realtime finite state machines (TFSMs). However, in most works where this class of real-time automata is studied a simple variant of TFSM semantics is used: the transduction relation computed by a TFSM is defined so that the elements of an output stream, regardless oftheir timestamps, follow in the same order as the corresponding elements ofthe input stream. This straightforward approach makes the model easier to analyze and manipulate, but it misses many important features of real-time computation. In this paper we study a more realistic semantics of TFSMs and show how to represent it by means of Labeled Transition Systems. The use of the new TFSM model also requires new approaches to the solution of verification problems in the framework of this model. For this purpose, we propose an alternative definition of TFSM computations by means of Labeled Transition Systems and show that the two definitions of semantics for the considered class of real-time finite state machines are in good agreement with each other. The use of TFSM semantics based on Labeled Transition Systems opens up the possibility of adapting well known real-time model checking techniques to the verification ofsequential reactive systems.

scholarly journals STRATEGY FOR SCALABLE SCENARIOS MODELING AND CALCULATION IN EARLY SOFTWARE RELIABILITY ENGINEERING

2015 ◽  
Vol 77 (9) ◽  
Author(s):  
Awad Ali ◽  
Dayang N. A. Jawawi ◽  
Mohd Adham Isa
Keyword(s):  
Software Reliability ◽  
Research Effort ◽  
System Modeling ◽  
Finite State Machines ◽  
State Machines ◽  
Reliability Engineering ◽  
Finite State ◽  
Early Design Stages ◽  
Behaviour Models

System scenarios derived from requirements specification play an important role in the early software reliability engineering. A great deal of research effort has been devoted to predict reliability of a system at early design stages. The existing approaches are unable to handle scalability and calculation of scenarios reliability for large systems. This paper proposes modeling of scenarios in a scalable way by using a scenario language that describes system scenarios in a compact and concise manner which can results in a reduced number of scenarios. Furthermore, it proposes a calculation strategy to achieve better traceability of scenarios, and avoid computational complexity. The scenarios are pragmatically modeled and translated to finite state machines, where each state machine represents the behaviour of component instance within the scenario. The probability of failure of each component exhibited in the scenario is calculated separately based on the finite state machines. Finally, the reliability of the whole scenario is calculated based on the components’ behaviour models and their failure information using modified mathematical formula. In this paper, an example related to a case study of an automated railcar system is used to verify and validate the proposed strategy for scalability of system modeling.

Sign in / Sign up

Export Citation Format

Share Document