Analysis of TLcharts for weapon systems software development

Download
Author
Demir, Kadir Alpaslan.
Date
2005-12Advisor
Drusinsky, Doron
Shing, Man-Tak
Metadata
Show full item recordAbstract
The success of formal specifications and reactive systems is highly dependant on the formal specification language being used. To date, the most common approach to this problem involves two activities: (i) the specification activity, where correctness properties are specified, and (ii) verification activity, where the system under review is proven to satisfy those properties. Typically, some form of temporal logic or regular expression language is used to specify the correctness properties; properties that are specified for given states of the system under review. This means that specification is partial and is done after system design, prototyping, or coding. Temporal logics have been found to be unsuitable for early specification. This thesis investigates the suitability of TLCharts, a specification language that combines statecharts and temporal logic, for the early specification of the dynamic characteristics of a homing torpedo. In order to achieve the task, a fictitious homing torpedo example, called KTorp, is used. Using a systematic approach, we developed deterministic statecharts and non-deterministic TLCharts for the KTorp control software. Our case study shows that using TLCharts as the early specification language for weapon systems software provides efficient, visual and intuitive specifications.
Collections
Related items
Showing items related by title, author, creator and subject.
-
A protocol validator for the SCM and CFSM models
Bulbul, Zeki Bulent (Monterey, California: Naval Postgraduate School, 1993-06);This thesis introduces and describes a software tool called Mushroom which automates the analysis of network protocols specified by the Systems of Communicating Machines (SCM) and the Communicating Finite State Machines ... -
Strategies for Application of the Coalition Battle Management Language (C-BML) with the Military Scenario Definition Language (MSDL)
Blais, Curtis (2012);The Coalition Battle Management Language (C-BML) is a common language for expressing and exchanging plans, orders, requests, and reports across command and control systems, modeling and simulation systems, and robotic ... -
XML based adaptive IPsec policy management in a trust management context
Mohan, Raj. (Monterey, California. Naval Postgraduate School, 2003-12);TCP/IP provided the impetus for the growth of the Internet and the IPsec protocol now promises to add to it the desired security strength. IPsec provides users with a mechanism to enforce a range of security services for ...