• Aug 25, 2016 News!Vol.4, No.3 has been published with online version. 15 peer reviewed articles from 3 specific areas are published in this issue.   [Click]
  • May 03, 2016 News!Vol. 3, No. 3 has been indexed by EI (Inspec).   [Click]
  • May 03, 2016 News!Vol. 3, No. 2 has been indexed by EI (Inspec).   [Click]
General Information
    • ISSN: 2301-3559
    • Frequency: Quarterly
    • DOI: 10.18178/LNSE
    • Editor-in-Chief: Prof. Jemal Antidze
    • Executive Editor: Ms. Nina Lee
    • Abstracting/ Indexing: EI (INSPEC, IET), DOAJ, Electronic Journals Library, Engineering & Technology Digital Library, Ulrich's Periodicals Directory, International Computer Science Digital Library (ICSDL), ProQuest and Google Scholar.
    • E-mail: lnse@ejournal.net
Editor-in-chief
Prof. Jemal Antidze
I. Vekua Scientific Institute of Applied Mathematics
Tbilisi State University, Georgia
I'm happy to take on the position of editor in chief of LNSE. We encourage authors to submit papers concerning any branch of Software Engineering.

LNSE 2013 Vol.1(2): 186-189 ISSN: 2301-3559
DOI: 10.7763/LNSE.2013.V1.42

A Component-Based Approach to Verification of Formal Software Models to Check Safety Properties of Distributed Systems

Sungeetha Dakshinamurthy and Vasumathi K. Narayanan
Abstract—In this paper, we model a distributed system consisting of n processes by a respective set of n Communicating Finite State Machines (CFSMs). The processes run concurrently and communicate with each other to accomplish a common goal. As opposed to the traditional product automaton built from the specified CFSMs, whose state-space explodes, we build a compressed model of what are defined as Communicating Minimal Prefix Machines (CMPMs) by simulating the CFSMs concurrently in parallel. The states of CMPMs form a well-founded, partial order. This model can be used to perform reachability analysis of the given system to check the safety properties such as communication deadlocks. The algorithm to generate the CMPMs model from CFSMs is presented in pseudo-code and its complexity discussed.

Index Terms—CFSMs, CMPMs, distributed-system, state-space explosion, reachability analysis, communication deadlocks.

S. Dakshinamurthy is with St. Joseph’s college of Engineering and Research scholar in Sathyabama University, India (e-mail:sungeetha5@yahoo.com).
V. Narayanan is with St. Joseph’s college of Engineering, India (e-mail: vasumathin@yahoo.com).

[PDF]

Cite: Sungeetha Dakshinamurthy and Vasumathi K. Narayanan, "A Component-Based Approach to Verification of Formal Software Models to Check Safety Properties of Distributed Systems," Lecture Notes on Software Engineering vol. 1, no. 2, pp. 186-189, 2013.

Copyright © 2008-2015. Lecture Notes on Software Engineering. All rights reserved.
E-mail: lnse@ejournal.net