VERIFICATION BY CONSECUTIVE PROJECTIONS

Date

1993-01-01

Author

HAGHVERDI, E
INAN, K

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

143
views

0
downloads

A new complexity relief technique for verifying formal specifications based on finite state machines is described. The method uses a Hoare's CSP-like nondeterministic semantics instead of the more commonly used observational equivalence and thus offers greater simplification without an essential loss of information. The approach is based on two algebraic operators on processes that perform parallel composition and process projection. It is shown that under appropriate conditions the complexity raising operation of parallel composition and the complexity reducing operation of process projection can be used alternately to keep the cumulative complexity within practical bounds. The merits of the technique are described via the dining philosophers problem through the concept of the composite philosopher. The method was implemented and applied to an example of alternating bit transport protocol. Presently the verifier implementation is being applied to problems of realistically larger sizes to assess its practical complexity reduction power.

Subject Keywords

Program verification, Tools and techniques, Requirements specifications, Software, Software engineering

URI

https://hdl.handle.net/11511/66132

Journal

IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS

Collections

Department of Electrical and Electronics Engineering, Article

Suggestions

OpenMETU
Core

A RECURSIVE PROCESS ALGEBRA FOR QUEUES YENIGUN, H; HAGHVERDI, E; BILGEN, S; INAN, K (1994-01-01) We present a new algebra for processes that involve queueing operations. The algebra uses operators from CSP with extensions that uses dynamical event alphabets [1] and a new process operator for modeling FIFO process queueing. Two methods are suggested for deriving a buffered automaton from a given I/O (Mealy) automaton and the second one is applied to derive a general algebraic model for an SDL program. The algebra has the power to express the global state of an SDL program in terms of an algebraic expres...
Design and fpga implementation of an efficient deinterleaving algorithm Olgun, Muhammet Ertuğ; Akar, Gözde; Department of Electrical and Electronics Engineering (2008) In this work, a new deinterleaving algorithm that can be used as a part of an ESM system and its implementation by using an FPGA is studied. The function of the implemented algorithm is interpreting the complex electromagnetic military field in order to detect and determine different RADARs and their types by using incoming RADAR pulses and their PDWs. It is assumed that RADAR signals in the space are received clearly and PDW of each pulse is generated as an input to the implemented algorithm system. Cluste...
Verification of Modular Diagnosability With Local Specifications for Discrete-Event Systems Schmidt, Klaus Verner (Institute of Electrical and Electronics Engineers (IEEE), 2013-09-01) In this paper, we study the diagnosability verification for modular discrete-event systems (DESs), i.e., DESs that are composed of multiple components. We focus on a particular modular architecture, where each fault in the system must be uniquely identified by the modular component where it occurs and solely based on event observations of that component. Hence, all diagnostic computations for faults to be detected in this architecture can be performed locally on the respective modular component, and the obt...
Verification and transformation of complex and uncertain conceptual schemas Yazıcı, Adnan (World Scientific Pub Co Pte Lt, 1997-12-01) In database environment it is necessary to represent complex and uncertain information at conceptual level and then transform the conceptual schema into the logical one for ultimate implementation. It is also important to verify the conceptual schema with respect to the constraints imposed on the schema definition. In this paper we primarily focus on the verification and transformation of the conceptual schema For the purpose of verification of the conceptual schema represented by the ExIFO data model (the ...
Derivation of length extension formulas for complementary sets of sequences using orthogonal filterbanks Candan, Çağatay (Institution of Engineering and Technology (IET), 2006-11-23) A method for the construction of complementary sets of sequences using polyphase representation of orthogonal filterbanks is presented. It is shown that the case of two-channel filterbanks unifies individually derived length extension formulas for complementary sequences into a common framework and the general M-channel case produces novel formulas for the extension of complementary sets of sequences. The presented technique can also be used to generate polyphase and multilevel sequences.

Citation Formats

E. HAGHVERDI and K. INAN, “VERIFICATION BY CONSECUTIVE PROJECTIONS,” IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS, pp. 465–478, 1993, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/66132.