Effective Extraction of State Invariant for Software Verification

2015 ◽  
Vol 752-753 ◽  
pp. 1097-1104
Author(s):  
Seung Su Chun
Keyword(s):  
Model Checking ◽  
Software Design ◽  
Finite State Machine ◽  
Software Verification ◽  
Software Systems ◽  
Reachable State ◽  
Early Integration ◽  
Finite State ◽  
Verification Techniques ◽  
User Focus

In software design of complex systems, more time and effort are spent on verification than on constructions. Model checking for software verification techniques offer a large potential to obtain and early integration of verification in the design process. This paper describes how to easily specify and the software properties and to understand the software generating automatically invariant. In this paper deal with issue that state invariant is a property that holds in every reachable state. Not only can be used in understanding and analysis of complex software systems. In addition, it can be used for system verifications such as checking safety, consistency, and completeness. For these reasons, there are many vital researches for deriving state invariant from finite state machine models. In this research was to be considered to extract state invariant. Thus it is likely to be too complex for the user to understand. This paper let the user focus on some interested parts (called scopes) rather than a whole state space in a model. Computation Tree Logic (CTL) is used to specify scopes in which he/she is interested. Given a scope in CTL, forward reachability analysis is used to find out a set of states inside it. Obviously, a set of states calculated in this way is a subset of every reachable state. Keywords: Software verification, Invariant, Scopes, Model Checking

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 Realization of Parallelism in a Sequential Legacy „C‟ Program

2020 ◽  
Vol 9 (2) ◽  
pp. 1179-1183
Keyword(s):  
High Speed ◽  
Finite State Machine ◽  
Research Work ◽  
State Machine ◽  
Parallel Processors ◽  
Software Systems ◽  
Functional Modules ◽  
Finite State ◽  
C Program ◽  
Computational Platform

In the present era of high speed computation with the multicore and other parallel processors in the computational field, there are still some organizations which rely on their old software systems developed years ago, which over the time have been subjected to continous development by different developers. Even though these softwares persist with the old and little in use technology, they still work to satisfy the operational demands of the organizations and have kept them going in the competetive industry. These systems which have with time grown into legacy, embed the major business functionalities of the organization, which is but effort of years. Hence a methodology is required to rebuild the legacy system to make them suitable for execution on to the present computation systems. The paper discusses a research work, wherein work is done to realize points of latent parallelism in a sequentially executing legacy ‘C’ program which is initially restructured and the design information abstracted. A technique using finite state machine is proposed to identify tasks, events, processes and jobs in the program, which helps to locate functionally independent computational units in the program. Furthur using the slicing technique, slicing is performed to extract out the appropriate lines of codes defined by the slicing criteria, which assembled together form a functionality that can be executed in parallel with other extracted functional modules or computational units on any parallel computational platform.

Model checking of finite-state machine-based scenario-aware dataflow using timed automata

2015 ◽  
Author(s):  
Mladen Skelin ◽  
Erik Ramsgaard Wognsen ◽  
Mads Chr. Olesen ◽  
Rene Rydhof Hansen ◽  
Kim Guldstrand Larsen
Keyword(s):  
Model Checking ◽  
Finite State Machine ◽  
Timed Automata ◽  
State Machine ◽  
Finite State

scholarly journals Application of genetic programming and model checking for finite-state machine induction

2014 ◽  
Vol 4 (15) ◽  
pp. 123 ◽  
Author(s):  
Anatoly Abramovich Shalyto ◽  
Fedor Nikolaevich Tsarev ◽  
Kirill Victorovich Egorov
Keyword(s):  
Model Checking ◽  
Genetic Programming ◽  
Finite State Machine ◽  
State Machine ◽  
Finite State

An EFSM Approach to Software Design Based on the Supervisory Control Theory

2012 ◽  
Vol 198-199 ◽  
pp. 557-561 ◽  
Author(s):  
Xiang Yun Wang ◽  
Kai Yuan Cai
Keyword(s):  
Control Theory ◽  
Software Design ◽  
Supervisory Control ◽  
Finite State Machine ◽  
State Machine ◽  
Sufficient Condition ◽  
Necessary And Sufficient Condition ◽  
Supervisory Control Theory ◽  
Finite State ◽  
Necessary And Sufficient

The research of software design, based on the supervisory control theory, is an important content in software cybernetics. The existing software model used in the software design with the supervisory control theory is Polynomial Dynamic System (PDS), which is transformed from SIGNAL files. This obstructs its widespread application. Extended Finite State Machine (EFSM) model is widely applied in software engineering field and it may alleviate the state explosion problem of Finite State Machine (FSM) to some extent. In this paper, the EFSM model is suggested to study software design problem. This paper proposed two kinds of software design problems based on EFSM model. For the first problem, a necessary and sufficient condition for software existence is obtained. For the second problem, a necessary and sufficient condition for software existence and an optimal algorithm to such software design are presented.

MARKOV MATHEMATICAL MODEL OF DYNAMIC ADAPTIVE TESTING OF AN ACTIVE AGENT

2018 ◽  
pp. 29-35
Author(s):  
N. V. Brovka ◽  
P. P. Dyachuk ◽  
M. V. Noskov ◽  
I. P. Peregudova
Keyword(s):  
Mathematical Model ◽  
Finite State Machine ◽  
Active Agent ◽  
Adaptive Testing ◽  
State Machine ◽  
Learning Activities ◽  
Independent Learning ◽  
Complex Object ◽  
Total Reward ◽  
Finite State

The problem and the goal.The urgency of the problem of mathematical description of dynamic adaptive testing is due to the need to diagnose the cognitive abilities of students for independent learning activities. The goal of the article is to develop a Markov mathematical model of the interaction of an active agent (AA) with the Liquidator state machine, canceling incorrect actions, which will allow mathematically describe dynamic adaptive testing with an estimated feedback.The research methodologyconsists of an analysis of the results of research by domestic and foreign scientists on dynamic adaptive testing in education, namely: an activity approach that implements AA developmental problem-solving training; organizational and technological approach to managing the actions of AA in terms of evaluative feedback; Markow’s theory of cement and reinforcement learning.Results.On the basis of the theory of Markov processes, a Markov mathematical model of the interaction of an active agent with a finite state machine, canceling incorrect actions, was developed. This allows you to develop a model for diagnosing the procedural characteristics of students ‘learning activities, including: building axiograms of total reward for students’ actions; probability distribution of states of the solution of the problem of identifying elements of the structure of a complex object calculate the number of AA actions required to achieve the target state depending on the number of elements that need to be identified; construct a scatter plot of active agents by target states in space (R, k), where R is the total reward AA, k is the number of actions performed.Conclusion.Markov’s mathematical model of the interaction of an active agent with a finite state machine, canceling wrong actions allows you to design dynamic adaptive tests and diagnostics of changes in the procedural characteristics of educational activities. The results and conclusions allow to formulate the principles of dynamic adaptive testing based on the estimated feedback.

PENERAPAN FINITE STATE MACHINE UNTUK PENGENDALIAN ANIMASI PADA VIDEO GAME RPG NUSANTARA LEGACY

2018 ◽  
Vol 3 (1) ◽  
pp. 1
Author(s):  
Mustofa Mustofa ◽  
Sidiq Sidiq ◽  
Eva Rahmawati
Keyword(s):  
Life Cycle ◽  
Video Game ◽  
Finite State Machine ◽  
Role Playing ◽  
State Machine ◽  
Game Development ◽  
Development Life Cycle ◽  
Finite State ◽  
Role Playing Game

Perkembangan dunia yang dinamis mendorong percepatan perkembangan teknologi dan informasi. Dengan dorongan tersebut komputer yang dulunya dibuat hanya untuk membantu pekerjaan manusia sekarang berkembang menjadi sarana hiburan, permainan, komunikasi dan lain sebagainya. Dalam sektor hiburan salah satu industri yang sedang menjadi pusat perhatian adalah industri video game. Begitu banyaknya produk video game asing yang masuk ke dalam negeri ini memberikan tantangan kepada bangsa ini. Tentunya video game asing yang masuk ke negara ini membawa banyak unsur kebudayaan negara lain. Ini semakin membuat kebudayaan nusantara semakin tergeserkan dengan serangan kebudayaan asing melalui berbagai media. Maka dari itu peneliti mencoba untuk menerapkan Finite State Machine dalam merancang sebuah video game RPG (Role-Playing game) yang memperkenalkan kebudayaan. Dalam perancangan video game ini peneliti menggunakan metode GDLC(Game Development Life Cycle) agar penelitian ini berjalan secara sistematis. Dalam suatu perancangan video game tedapat banyak elemen, pada penelitian ini penulis lebih fokus pada pengendalian animasi karakter yang dimainkan pada video game ini. Dari perancangan yang dilakukan, disimpulkan bahwa Finite State Machine dapat digunakan untuk pengendalian animasi yang baik pada video game RPG. Diharapkan video game ini dapat menjadi salah satu media untuk mengenalkan kebudayaan nusantara

Human action recognition using simple geometric features and a finite state machine

2013 ◽  
Vol 18 (2-3) ◽  
pp. 49-60 ◽  
Author(s):  
Damian Dudzńiski ◽  
Tomasz Kryjak ◽  
Zbigniew Mikrut
Keyword(s):  
Action Recognition ◽  
Finite State Machine ◽  
Recognition Rate ◽  
Human Action Recognition ◽  
Human Action ◽  
Video Stream ◽  
State Machine ◽  
Recognition Algorithm ◽  
Finite State ◽  
Correct Recognition Rate

Abstract In this paper a human action recognition algorithm, which uses background generation with shadow elimination, silhouette description based on simple geometrical features and a finite state machine for recognizing particular actions is described. The performed tests indicate that this approach obtains a 81 % correct recognition rate allowing real-time image processing of a 360 X 288 video stream.

Sign in / Sign up

Export Citation Format

Share Document