Model Based Specification CIS 376 Bruce R Maxim UM Dearborn Model Based Specification Overview System model defined using well understood mathematical entities like sets and functions System state is not hidden like it is in algebraic specification State changes are straight forward to define VDM and Z are the most widely used modelbased specification languages Z Formal Language Based on set theory and first order predicate logic Strongly typed Declarative language Makes use of a graphical construction known as a schema provide an effective low level structuring facility are useful as specification building blocks can be understood fairly easily Schemas Include a unique name or identifier a signature that declares entities and their types a predicate part that defines invariants involving these entities Schemas can be included in other schemas and act as type definitions Names are local to the schema in which they are defined Schema Declaration Part Contains local declarations types and variables Can import other types by listing their names Anonymous schemas name omitted are used to make global declarations Anonymous schemas usually do not contain a predicate part Schema Predicate Part Statements about the entities defined in the declaration part of the schema These statements must be true at all times Multiple statements are assumed to be implicitly connected by a logical and Other logical connectives e g or implies equivalent etc can be used explicitly in compound statements Z specification examples were posted on the World Wide Web by Ken Abernathy Furman University Example Schema The symbol P is used to indicate the power set of a type and the symbol is used to define a relation between two types i e a set of ordered pairs from the Cartesian product of the two types IO Channel Assignments Basic Types active instruments P Platform Instruments assigned to Communications Channels Platform Instruments available busy P Communications Channels range assigned to subset of active instruments available busy Z Lexical Elements Character set includes all keyboard characters and special mathematical symbols Identifiers must begin with a letter and may contain any number of digits letters upper and lower case and the underscore Identifiers may have suffixes input variable output variable new value for variable following a state change Z Types and Declarations Built in types the integers denoted by Z natural numbers 0 1 2 denoted by N positive integers denoted by N1 the reals are not a built in type Free types similar to enumerated types in C Basic types aka unspecified types Z Operators part 1 Operator denotes the cardinality of a finite set Operator is used to extract ordered pairs from a relation having specified first coordinate values Example channel assigned to 5 This statement asserts that the number of pairs from the relation assigned to whose first coordinates equal the value of the input variable channel is less than 5 Z Operators part 2 The operator functions almost like except it extracts pairs from a relation based on the value of the second coordinate Example assigned to instrument 3 This states that the number of ordered pairs from the relation assigned to whose second coordinates equal the value of the input variable instrument is less than 3 Z Operators part 3 The notation a b is used to denote a specific potential pair in a relation instead of the more standard ordered pair notation a b The following notation is used for the relational image operator range set Example assigned to channel In this example the relational image operator returns the image in the range set of the value of the variable channel for the relation assigned to Creating New Schemas from Existing Schemas The prefix Delta is used to create a new schema from an existing one A Delta schema is obtained by combining the before and after specifications of a state The prefix Xi is also used to create a new schema from an existing one Similar to a Delta schema an Xi schema is obtained by combining the before and after specifications of a state However this schema is used to define specifications of operations such as inquiries that do not change the state of a structure Delta Schema Example IO Channel Assignments Basic Types active instruments active instruments P Platform Instruments assigned to assigned to Communications Channels Platform Instruments available available busy busy P Communications Channels ran assigned to subset of active instruments ran assigned to subset of active instruments available busy available busy Xi Schema Example IO Channel Assignments Basic Types active instruments active instruments P Platform Instruments assigned to assigned to Communications Channels Platform Instruments available available busy busy P Communications Channels ran assigned to subset of active instruments available busy active instruments active instruments assigned to assigned to available available busy busy Operation Specification Options Operations may be specified incrementally as separate schema and then combined to produce a complete specification Define a normal operation as a schema Define schemas for exceptional situations Combine all schemas using a disjunctive or operator Importing Delta and Xi Schemas Importing and schemas into operation specifications provides a way to record the intended impact of the operations on state variables and predicate Provides a built in check on the result of an operation Z Specification Process Define given sets and ty pes Write informal specification Decompose sy stem Specify sy stem components Compose component specifications Define state variables Define initial state Define correct operations Define exceptional operations Combine operation schemas Example Problem A space platform contains a number of instruments Several communications channels are provided allowing both input and output instrument communications Platform instruments may be placed in active or inactive states Only active instruments may be assigned to I O channels Active instruments may be assigned to more than one I O channel up to some maximum number of I O channels per instrument I O channels may be shared by several active instruments up to some maximum number of instruments shared per I O channel Basic Variables and Invariants IO Channel Assignments Basic Types active instruments P Platform Instruments assigned to Communications Channels Platform Instruments available busy P Communications