Analysis of TLcharts for weapon systems software development
Demir, Kadir Alpaslan.
MetadataShow full item record
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.
Showing items related by title, author, creator and subject.
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 ...
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 ...