Introduction

mini-index of document

Literature Basis

The For's
The Againsts
Why Both School's are Right
Other Connectivity Issues

Proposed Approach

Benefits

partitions represent characteristics of algorithms (hw or sw) or data type's underlying structure
integrated specs
programmer usually concerned with functionality
  1. specification slippage can occur
  2. reasoning based on specification becomes invalidated with slippage
  3. possibly reduce slippage (for some programming tasks based on specification)
  4. or eliminate it (for simple aspects of correspondence between spec and implem, such as that a particular number of outcomes are implemented by an operation)
Superiority to Ada without analysis/synthesis
automatic checks on some things programmers commonly forget
  1. automatic firewall code for important operations
  2. code fragments to be included can be rigorously verified for particular properties off-line, rather than incurring compiler overhead time working on them.
verification
develop methods for totalization
  1. develop libraries with some properties verified
  2.  
  3. The consequence model embodies a unified mechanism for connecting program operations. This is beneficial because it can be a simplification over the complex behavior exhibited by program with a mixture of procedural/functional returns, exception handling and message passing. The success of the model will hinge largely on whether the features of the model can be provided to the programmer in an elegant and useable form.
  4. The consequence model has more connections determined statically within the program than an equivalent program based on exception handling. Exception handling can use a static approach too, or the consequence model could not call upon it to enforce the model. However, in exception handling, the static approach is not an automatic given; one must extremely carefully consider the placement of firewalls and exception handlers in order to ensure this behavior. The consequence model is an advantage over this because most of this detailed structuring is inserted by the translator into the final program. The analysis that would be required every time in the exception handling approach can be done very carefully once for the fragments to be inserted by the translator.
  5. Total operations can be a beneficial method for recording important specification information in a form that resides with the program. By forcing the programmer to interact with this specification, it is possible that the specification and the program can be kept synchronized. If the specification and code are separate, it is difficult to make sure that the specification continues to accurately describe the behavior of the program.
Benefits Thoughts
Using Total Operations to Build Hierarchical Subsystems
Iterative Specification Creation

Research Plan

Research

  1. Show Equivalence with Turing Machine
  2. Compile a Set of Desirable Control-Flow Properties
  3. Prove by Rigorous Argument that These Properties Hold for the Code Fragments
  4. Translate Rigorous Arguments into Formal Proofs for Properties
  5. Represent Consequence Model in Formal Specification Language

Development

  1. Implement Ada parser
  2. Implement ZENO translator
  3. Implement ZENO Graph Model
  4. Implement Example Parts with ZENO
  5. Implement ZENO Verifier

Evaluation

  1.  
  2.  
Lower level interfacing
enforce certain characteristics of system use by supplying consequence wrapper
  1. how does this affect productivity & reuse?
  2. does it assist in stopping errors?
Prove a few interesting properties in examples
heap properties using own heap form
  1. all control paths
  2. result correctness on a path
development process
guide programmer through process
  1. requirements for passing between phases of development
Research Plandendum
  • The overall proposed research is to develop a specification language that supplements the Ada programming language by allowing total operations to be defined, used and verified for important properties. This will involve developing the consequence model more completely and developing the tools to support the model. The primary tools that create Ada programs from ZENO specifications are the translator and the verifier. These are depicted in Figure See Primary ZENO Tools.
  • <the figure is screwed; pull in the nice picture from the defense slides.>
  • <make sure this figure is totally represented in that figure.>
  • <conciser and cleaner and better and morer>
  • The following research goals will be addressed:
An Operation Model Based on Total Operations
  • Development of Total Operation Model
  • Development of Syntax for Model
  • Development of Method of Application of Model
  • Evaluation of approach
Ada Translator for Total Operation Specifications
  • Implement Ada Parser
  • Implement Objects to Support consequence model
  • Implement Dependable Code Fragments Used by Translator
  • Devise Set of Compile-Time Checks for Specifications and their Implementations
  • Implement Interface to Verifier
Property Verification
  • Isolation of Important Application-Independent Properties
  • Provide Syntax for Stating Critical Properties
  • Develop Prototype Verifier
  • Apply Verifier to Existing Ada System for Specified Properties
  • Evaluate Verification Capability
Verifying Programs Based on Total Operations
  • Verifying properties for critical program components is a necessary antecedent to producing dependable software. An operation in the consequence model can be analyzed by tracing each possible data flow path from its operands to each of its consequences. The characteristic predicate for the result produced by each operation invoked on a particular path yields a composite statement of the consequence's result. This composite statement can be entered into a theorem prover to assess whether the specification of the consequence is implemented by the operations composing that path (or group of paths) through the operation.
  • If the implementation of a consequence's result or outcome cannot be proven to conform to its specification, then there are four possibilities:
  • the conformance cannot be proven because the specification is incorrect,
  • the conformance cannot be proven because its proof is impossible,
  • the operation is incorrectly implemented on the path for that consequence, or
  • the available theorems are not sufficient to prove them.
  • To minimize the impact of the first case, specification consistency checking tools could help to locate certain types of incorrectly stated consequence specifications. For example a tool might point out where outcome specifications intersect or where subsets of the domain are not covered. The second case is a possibility given Gödel's incompleteness theorem, but few cases of this sort are expected because operation specifications are usually too simple to induce a logical system of sufficient complexity. In the third and fourth cases, the verification tool should point out the path along which the verification breaks down. The development of more efficient diagnostics for reporting non-verified consequences is a goal of this research.
  • Certain property verifications are necessary in dependable systems. The consequence model directly assists in the necessary verifications because it is formal, precise, and unambiguous. The reliance that can be placed upon the verifications performed for operations based on consequences is as strong as the reliance that can be placed upon the operations composing them and upon the underlying hardware of execution (to paraphrase Hoare quoted in []).
Toolset
  • To assist designers in using ZENO to specify programs, a set of tools is necessary. These tools are not intended to provide an entire design and run-time environment, but are used to add ZENO specifications to Ada programs and then verify properties of the programs. Instead of relying on Ada's exception handling model, a designer can specify an operation's consequences using ZENO and then implement the algorithmic portions of the operations in Ada. The ZENO specifications are embedded in the Ada interface specifications for the packages and subprograms making up the design, and a full program implementation is constructed by putting together the Ada algorithms with the basic structures that implement the properties specified in ZENO notation. The toolset makes this process easier and free of common errors.
  • The toolset includes:
Specification Checker
  • There are a number of properties that must hold for the definition of an operation, or that operation cannot be called ``well-specified'' within the model. These properties have effective algorithms for detecting whether the operation is well-specified or not, and each necessary property is checked before allowing the full Ada implementation of the program to be constructed.
Visualizer
  • A data-flow graph can be constructed from operation specifications. The visualizer produces this graph and displays it on an appropriate graphic display device. The visible data-flow graph is useful for examining the connections and interactions within a design, and for obtaining an overview of a design's structure. Zooming in and out of operations will be supported to allow the entire design to be traversed and inspected. The outermost view depicts an entire non-concurrent program as a single operation, while the lower-level operations contained within it can be individually zoomed into and inspected.
Verifier
  • The verifier attempts to prove that the consequences specified for an upper-level operation are actually implemented by the operations composing it. Using existing proof techniques, the verifier shows that:
the operand space is partitioned by the specification for the operation's outcomes,
  1. the operation does not violate its specification by modifying inappropriate operands,
  2. the properties of each consequence are guaranteed by the specifications of the operations used to implement that consequence,
  3. zones do not observe or modify elements unless they are passed to it in an operand message,
  4. zones that are specified as infinitely operating servers are implemented as such, and
  5. communication between zones does not degrade due to badly specified message dependencies.

Definitions

Computational Model

Element
  • A member of a data type, where the data type can be composed from other data types. For example,
  • .
Variable
  • A relation between a name and an element. The element is also referred to as the variable's value. A value that is possible for any variable is called "undefined;" this corresponds to the variable's value when the variable's name exists but that name has not yet been associated with an element. Every variable has a storage location where its value is kept.
Scope
The collection of threads where a variable's name is visible according to the target language's scoping rules.
Environment
A set of variables, e.g. (n → 20, y → "input.dat").
Operation
A computational action applied to an environment yielding a possibly different environment.
Program
A finite sequence of operations.
Execution point
A numerical index (into a program).
Thread
A triple containing a program, an execution point and an environment.
Control flow
A relation between a thread and an execution point within the same thread.
Data flow
A relation between a sequence of threads and a thread.
Connection
A data flow between two operations caused by a program. The "sending" operation is called the predecessor and the "receiving" operation is called the successor.
Discussion of Computational Model Definition
  • This section has set down the definitions for several common programming terms that will be used as the basis for defining the consequence model.
  • The concept of a "program" that is defined here is a simplification of what is commonly considered to be a program, but the definition of a program as a sequence of operations is sufficient for general programs; block structure and other complications can be encoded as a set of operations that transform the program's environment as desired. Programs are commonly encoded in a computer's machine language, which has a structure distinctly resembling a sequence of operations with an environment and an execution point.
  • The definition for data flow points to the fact that a data flow operation's parameters can flow to the operation from numerous other operations. The data flow operation will not "fire" until all of its required parameters are present. Control flow can be seen as a special case of this where only one thread passes the parameters to the operation simultaneously. If a program is executed on a uniprocessor machine, then the interpretation of data flow on this machine is equivalent to control flow.

Consequence Model

Operand
  • An variable travelling by data flow to an operation where the operation observes and/or modifies the storage location and/or value of the variable. For example, in the addition expression (a + b), a and b are operands to +. In the assignment statement (c = d), c and d are operands to = and c's contents are modified.
Characteristic Predicate
  • A formal predicate logic statement in a formal specification language that is used to describe theoretical properties within the program1. For example,
  • and are both characteristic predicates in Z.
Operand Space
  • The n-dimensional space generated by the cross-product of an operation's operand types. This is also called the input domain. For example, the operand space for an integer addition operation is the set { Integer × Integer } and contains elements such as (3,5) and (-30, 8).
Result
  • An element computed by an operation that is passed through a connection to a successor. Results are specified using a characteristic predicate. For example, Result ::=
  • or Result ::= . The second example specifies a set containing all elements with the same type as the elements of the sequence N that are not contained in the sequence N at any of the indices listed in a set Q.
Result Space
  • The discriminated union of a set of results. A member of the result space has a type and value dictated by one member of the set of results.
Modification
  • A change to an operand that is described by a characteristic predicate. The operand becomes (or is assigned) the value specified in the predicate. For example,
  • and are both modification statements. From the perspective of the operation, modifications occur at points defined by the source code. From the perspective of the operation's invoker, modifications occur before the operation returns.
Outcome
  • The guard on a connection that allows data flow when a characteristic predicate evaluates to TRUE. For example, data would flow on an outcome with a predicate
  • when a=2, b=5, and c=3.
Consequence
  • A triple containing a result, an outcome, and a set of modifications. The meaning is that when the outcome's specified predicate evaluates to TRUE, then the specified modifications are made before the specified result is passed along the outcome's connection.
Well-Formed Consequential Operation
  • A computation that: 1) has a specification listing the number and type of all operands, 2) has a specification for all consequences, 3) always concludes with exactly one of the consequences, and 4) has an operand space partitioned by the set of consequences.
Total Operation
  • A relation from an operand space to a result space that is total. The valid or defined domain of the relation is thus equal to the operand space. The preconditions for a total operation are thus just {TRUE}, while the postconditions are partially specified by the consequences2. The well-formed consequential operation as defined above is a total operation.
Discussion of Consequence Model
  • <deverbosify>
  • <add block structuring/conseq types/other tasties>
  • <include defense denosem domains in separate appendix?>
  • This section has defined the consequence model. The name consequence has been chosen because it implies a situation that is fully determined by a prior set of conditions. It reaffirms the fact that a specification for an operation should be defined in terms of what the programmer intends to definitely happen when the operation is invoked. This is intended to counteract the connotation of an exception as an unusual or abnormal event; instead, a particular set of consequences is to be expected ahead of time from the specification of the operation.
  • The notion of an operation is recursive. An operation can represent primitive computations provided by a particular programming language or computer, or it can be used to represent complex computations that are composed from multiple lower-level operations. Operations have both a specification and an implementation, although clearly the implementation of some primitive or system operations might not be available for inspection.
  • -------------
  •  
  • Developing methods for enforcing that operation specifications define a true partition is one of the goals of this research.
flow
  1. extend static & dynamic notions to connectivity
anomalies formal definition
control flow model using control point
  1. statement of properties in terms of model
  2. detection of bad things, proof of good things
  3.  
  4. Different outcomes arise because the operand space is naturally or artificially partitioned into equivalence classes. A natural partition is one in which the nature of the data object generates the partition. An artificial partition is one where lower level implementation details (such as hardware support for mathematical operations) cause subsets of the input domain to be differentiated. The equivalence classes categorize the sets of elements that must be treated differently from other sets due to the operation's implementation or due to the definition of the operands. Each outcome might need different treatment by the invoker, and thus each outcome is represented as a separate data flow path leaving the operation.
  5. The consequence is the semantic construct in this model that is analogous to the exception. However, the programmer defines consequences more rigorously than exceptions are defined in conventional programming languages. A consequence specification details exactly what an operation accomplishes when it concludes with that consequence by describing the cause of the consequence (the outcome), the service provided by the consequence (the result), and how the parameters are changed when the operation completes (the modifications).

Verification Definitions

anomaly
A residual fault in a program implementation that can cause the specification for the program to be violated.
property
A characteristic of a program implementation.
property proof
A formal argument that a program possesses a particular property.
verification
The establishment of a set of property proofs for a program.
Discussion of Verification Definitions
  •  

Total Stack

a stack is full iff the used extent is all slots and forall slots, an element is stored in the slot.
  1. a stack is empty iff the used extent is all slots and forall slots, no element is stored in the slot.
  2. a stack is erroneous if therexists a slot that is within the used extent of the stack that has no element in it or if therexists a slot that is not within the used extent of the stack that has an element in it or if the counter of the used extent contains an impossible (negative or too large) value.
  3. a stack is partially-full iff a) its used extent is less than the whole stack and greater than the empty stack, b) forall used slots, there is an element in the slot and c) for all unused slots, there is no element in the slot.
  4. Showing that this set of axioms partitions all stacks requires showing that the abstract representation for a stack is partitioned by the axioms. This is the model for the stack in terms of concepts, rather than in terms of specific software or hardware representations. The abstract representation for a stack is an integer counter and an array of storage locations. The counter represents how many of the storage locations are used starting from the first location and progressing sequentially through the array.
  5. Given that the only two components inside a stack object are its counter and its array of elements, then the axioms above partition the stack. An informal proof is that all invalid counters are treated in case 3, and that the cases 1 and 2 are the boundary conditions for valid counters and valid content placements, while case 4 is all middle values between these two extremes for valid counters. Besides treating invalid counters, case 3 also treats all forms of invalid content placement. These content placements have either a hole where an element should be or they have a filled slot that is not supposed to be in use.
  6. The abstract representation must also be shown to map to a concrete representation in which the partition also holds. The concrete representation is still quite abstract; the most concrete level addressed here will be an underlying programming language representation of the object in question.
  7. <note that content validity not treated...>
  8.  
  9. Part of verifying this stack object might be showing that no valid combination of stack operations results in an erroneous stack. The sets of valid stack combinations are where the partial nature of the stack data type comes in, but the operations on the stack are still total operations.
  10. Note that the axioms do not prohibit the contents of the stack indices to be wildly different from whatever was stored there, but the result portions of the specifications for the stack consequences can be shown to ensure that the elements are stored appropriately. Given protection of the internal stack data, the contents can be assumed not to change except by the operations defined on the stack.
  11. If the set of axioms for combining operations on an object are themselves total, then all uses of the object can be categorized as valid or invalid based on the axioms?
  12.  
  13. The theorem set generated by the ??
  14. A stack push operation can add an element to an empty stack and to a partially-full stack, it cannot add to a full stack. Thus, the partition for the push operation has two equivalence classes that might be called Full and Non-full, where Non-full incorporates both empty and partially-full. Likewise, a stack pop operation cannot remove an element from an empty stack, but can from the other two kinds. The Pop operation's partition therefore might have two equivalence classes called Empty and Non-empty.
  • The three common operations on stacks are depicted in Figure See Three Stack Operations. The result specifications are based on an array-like notation for a stack. The `+' operator represents a concatenation of the stack and a new element. The `-' operator represents the removal of an element from the stack. The brackets operator extracts a single element from the stack at a particular position. Size is the current number of elements on the stack.
  • These three operations are each total.
  •  

1. The term "theoretical" is used here to signify that an operation might be intended to have a particular characteristic, but does not necessarily possess that characteristic.

2. To state that the postconditions are totally specified by the consequences would imply that the consequence specification is totally correct. Since the validity of the concept of total correctness is questionable, this work is focussing on aspects of partial correctness. Total operations are therefore robust, but not necessarily totally correct.