Verifying the interface compliance of federates using pre- and postconditions of RTI services

2009-12-01
Kizilay, Vijdan
Oguztüzün, Halit
Oğuztüzün, Mehmet Halit S.
Buzluca, Feza
The Federation Architecture Metamodel (FAMM) provides a domain specific language for describing the architecture of a High Level Architecture (HLA) compliant federation. A federation architecture model (FAM) consists of the object models and the behavioral models of participating federates. The communication behavior of each federate is to be modeled in the same level of detail as the HLA Federate Interface Specification so as to facilitate standard-compliant code generation. However, this level of detail increases the likelihood of the modelers making mistakes in following the standard. Thus, beyond well-formedness, static checking of the well-behavedness of federate behavioral models is desirable. If it can be shown that all the preconditions of the HLA Runtime Infrastructure (RTI) services used in a behavioral model are satisfiable then we have some assurance that the interface behavior can be compliant to the HLA Federate Interface Specification. In this paper, we present a model checking based procedure to verify the interface behavior of an HLA federate modeled in FAMM. Verification is performed automatically by the help of (1) a model interpreter that takes a FAM as input, and generates the PROMELA model of its behavioral part as output, (2) the SPIN model checker that performs model checking given the generated PROMELA process as input and then outputs the verification result in terms of the preconditions that will not hold at run-time. Copyright © (2009) by SISO - Simulation Interoperability Standards Organization.
Fall Simulation Interoperability Workshop 2009, 2009 Fall SIW

Suggestions

Layered simulation architecture: A practical approach
Topcu, Okan; Oğuztüzün, Mehmet Halit S. (2013-03-01)
This article presents a practical approach to the design of federate architectures for the simulation developers by applying a well-known architectural style, layered architecture, from a developer's perspective. Adopting layered architecture for an HLA-based simulation (i.e. a federate) provides a clear separation to the following concerns; the user interface (where the user can be a human or an external system such as a GIS server), the simulation logic, and the HLA-specific communication. Thus, layered s...
Visual behaviour during perception of architectural drawings: Differences between architects and non architects
Albayrak Colaço, Canan; Acartürk, Cengiz (2018-07-04)
Architectural design is not just a technical process based on problem-solving and representation, but also a social process distributed between architect and non-architect stakeholders. In this study, visual behaviour differences between architects and non-architects during perception, interpretation and evaluation of architectural drawings are analysed. An eye tacking experiment was conducted on two groups of participants: 19 graduate level students of the Department of Architecture and 19 students from ot...
Metamodeling of Reference Software Architecture and Automatic Code Generation
Turhan, Nafiye Kubra; Oğuztüzün, Mehmet Halit S. (2016-12-02)
Architectures of all application software that are developed by Sea Defense Systems Software Team in ASELSAN are created based on a predefined reference software architecture. In order to facilitate the process of transition from the software architectural design, which is created in conformance with the reference software architecture, to implementation a model driven software development approach is put forth. In this approach, based on a metamodel for the predefined reference software architecture, a dom...
Modeling of software as a service architectures and investigation on their design alternatives
Öztürk, Karahan; Doğru, Ali Hikmet; Department of Computer Engineering (2010)
In general, a common reference architecture can be derived for Software as a Service (SaaS) architecture. However, while designing particular applications one may derive various different application design alternatives from the same reference SaaS architecture specification. To meet the required functional and nonfunctional requirements of different enterprise applications it is important to model the possible design so that a feasible alternative can be defined. In this thesis, we propose a systematic app...
Nonblocking hierarchical control of decentralized des
Schmidt, Klaus Verner; Moor, Thomas (null; 2005-12-01)
This work considers a hierarchical control architecture for a class of discrete event systems which can also be applied to decentralized control systems. It is shown that nonblocking supervisory control on the high level of the hierarchy results in nonblocking and hierarchically consistent control on the low level. Copyright © 2005 IFAC.
Citation Formats
V. Kizilay, H. Oguztüzün, M. H. S. Oğuztüzün, and F. Buzluca, “Verifying the interface compliance of federates using pre- and postconditions of RTI services,” Orlando, FL, USA, 2009, Accessed: 00, 2021. [Online]. Available: https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=84865581577&origin=inward.