Development of Automated Systems using Proved B Patterns

2013 ◽  
pp. 125-139
Author(s):  
Olfa Mosbahi ◽  
Mohamed Khalgui ◽  
Zhiwu Li
Keyword(s):  
Formal Specification ◽  
Design Patterns ◽  
Software Component ◽  
Specification Language ◽  
Automated Systems ◽  
Formal Specification Language

This chapter proposes an approach for reusing specification patterns for the development of automated systems composed of two components: the controller and the controlled parts. The first is a software component controlling the second one that models the physical device and its environment. Specification patterns are design patterns that are expressed in a formal specification language. Reusing a specification pattern means instantiating it and the proofs associated. This chapter shows through a case study how to define specification patterns in Event-B, how to reuse them, and also how to reuse the proofs associated with specification patterns.

Extending Linear Temporal Logic with Clocks to Object-Z

2014 ◽  
Vol 513-517 ◽  
pp. 927-930
Author(s):  
Zhi Cheng Wen ◽  
Zhi Gang Chen
Keyword(s):  
Real Time ◽  
Temporal Logic ◽  
Formal Specification ◽  
Large Scale ◽  
Linear Temporal Logic ◽  
Specification Language ◽  
Continuous Variables ◽  
Real Time System ◽  
Software Specification ◽  
Formal Specification Language

Object-Z, an extension to formal specification language Z, is good for describing large scale Object-Oriented software specification. While Object-Z has found application in a number of areas, its utility is limited by its inability to specify continuous variables and real-time constraints. Linear temporal logic can describe real-time system, but it can not deal with time variables well and also can not describe formal specification modularly. This paper extends linear temporal logic with clocks (LTLC) and presents an approach to adding linear temporal logic with clocks to Object-Z. Extended Object-Z with LTLC, a modular formal specification language, is a minimum extension of the syntax and semantics of Object-Z. The main advantage of this extension lies in that it is convenient to describe and verify the complex real-time software specification.

Modeling and Reasoning about Design Patterns in Slam-Sl

2011 ◽  
pp. 206-235
Author(s):  
Angel Herranz ◽  
Juan José Moreno-Navarro
Keyword(s):  
Formal Specification ◽  
Design Pattern ◽  
Design Patterns ◽  
Formal Model ◽  
Specification Language ◽  
Class Operator

In this chapter, a formal model for Design patterns is studied. The formal specification of a Design pattern is given as a class operator that transforms a design given as a set of classes into a new design that takes into account the description and properties of the Design pattern. The operator is specified in the Slam-Sl specification language, in terms of pre and postconditions. Precondition collects properties required to apply the pattern and postcondition relates input classes and result classes encompassing most of the intent and consequences sections of the pattern. Formalization is mandatory for reasoning about Design patterns and for implementing assistant tools.

Sign in / Sign up

Export Citation Format

Share Document