Transcript PowerPoint

Background information
• Formal verification methods based on theorem proving techniques and
modelchecking
–
–
to prove the absence of errors (in the formal model)
to reason about the behaviors of programs
• No known generic software verification
–
–
Involves complicated proving
Generally cannot be easily and cost-effectively integrated to software and hardware
development cycles
Major Verification Topics
• Specification Verification
• Architecture Verification
• General practical issues
Architecture Verification
• Correctness of architecture refinement
– a methodology for the correct stepwise refinement of software
architectures
– using the approach of architecture refinement patterns that are
correctness preserving and compositional
Common architecture Issues
• From abstract level to concrete level
• Simple architecture: box - arrows, representing data
component and connections
• Large architecture: Hierarchical approach
Common architecture problem
• Limited utility of architecture hierarchy results from the
current level of informality
• Ambiguity in architecture allows unintended
interpretations. May cause erroneous interrepretation
Architecture Refinement
• From a abstract architecture to a concrete (lowerlevel) architecture
– lead to:
• fewer architectural design errors
• extensive and systematic reuse of design knowledge and proofs
Refinement pattern approach
• A pair architecture schemas (homogenous or heterogeneous)
• proven to be relatively correct with respect to the given mapping
schema
Refinement pattern
• Requires a special correctness criterion
– a special mapping between architectures
– extensive translation:
• the representation of components, interfaces, and
connections
• aggregated, decomposed, or eliminated
Completeness assumption
• Prove that a concrete architecture has all required
properties
– No new properties can be inferred from the concrete architecture
• All components, interfaces, and connections intended to be
true of the architecture at its level of detail
– If a fact is not explicit in the architecture, assume that it is not
intended to be true
Completeness assumption
• Standard way to proof relative correctness
– show that the concrete specification logically implies the abstract
specification under a given mapping
– allow additional and specified behaviors, as long as the specified
behavior is implemented
– no guarantee that negative properties are preserved under
refinement
• Alternative:
– faithful interpretation
– hard and no general proof technique
• Use preproved refinement patterns
Example
• Use only logical theories for simplicity
• To show how to systematically and
incrementally transform a abstract
architecture to its lower-level form
• Approach: combining small and local
refinement to form the larger composite
Example
chars
Lexical
Analyzer
toks
Lexical
Parser
bindings
ast
Analyzer
Optimizer
ast
Code
Generator
code
Example: abstract
sub-architecture to concrete subarchitecture
Lexical
Parser
ast
Analyzer
Optimizer
From simple dataflow to
shared syntax tree:
Architecture as Theories
• Architecture Styles
– Operations & axioms
• Translation to Logic
– Patterns  logic (theory generation rules)
• Mapping
– Name mapping
– Style mapping
– Interpretation mapping
Architecture styles
Dataflow style:
Axioms example -- Every function must at least have one port:
Translation to Logic
• An instance of function declaration schema:
– f: Functional_Style!Function [  op: t]
• The underlying theory contains the same instance of first order
sentences:
Pattern of Abstract Architecture
M: MODULE [
Pattern of Concrete Architecture
Mapping
• Name mapping:
– c | m
– op | w
• Style mapping:
– Accepts (_, _) | Gets (_, _)
– Connects (_, _, _) | Writes (_,_) ^ Reads(_,_)
• Interpretation mapping = name + style mapping
Proving
• Criterion
– all intended to do
– not intended to do
Composition
• Horizontal
– compose instances of refinement patterns to
form one large composite refinement
• Vertical
– most concrete architecture in a hierarchy is
correct with respect to the most abstract
– justified since faithful interpretation is
transitive
problem example
• Concrete architecture 1
– A  B (dataflow connection)
• Concrete architecture 2
– B  C (dataflow connection)
• the composition of 1 and 2 is not faithful!
– need new abstract dataflow from A to C
Specification
• Correctness issue
• Complete specification of program is in terms of
hierarchical structure of module specifications
• Module external specification are abstract, about module
behavior
• Module internal specifications are descriptions of internal
implementations
Concurrent System Verification
•
•
•
•
Program is a set of events
Interpreted and verified with a formal proof system
Internal specification classified as composite or simple
Composite: composed of linked sub-modules, each with
external and internal specification
External Specification
External specification consist of three parts:
• behavior: module delivers to the environment
• provide: how modules synchronizes with the environment
• require: synchronization cooperation the module expects
from environment
Composite internal specification
Internal specification of a composite module associates events
described in the external specification of the module with
events described in the external specifications of the submodules.
• Ports: a set of single direction communication channels
between the module and its environment
•Network link: sub module ports are connected together to
form communication channels
Composite module verification
Verification of composite module:
1. External behaviors of the sub-modules plus the network
and interface links must imply the external behavior of
composite module
2. Provides and requires of the sub modules and composite
module must be mutually supportive and complete.
“mutual support: sub module provides imply the sub- module
requires.
“ complete:composite require and provide represent the sub
module requires and provides accurately and completely.
Composite module
Simple module specification
verification
Internal specification of a simple consists of three parts:
• program: internal specification as example
• performance: whether the program is cyclic or terminates
and contains an assert statement that describe the history
• interpret: identify ports with subsequences on the history
Simple module internal specs
Simple module specification
verification
Verification of specifications of a simple module:
1. Performance and interpret statements must imply the
external behavior
2. Performance and external provide must be established
using following axioms :
• History Sequence Axiom
• Statement block Axiom
• Process history Axiom
Discussion
• Task of analyzing programs is easier if the program is
composed of modules
• Key importance is to establish specifications
• Automated verification system can be based on verification
rules
Related works
• Automatic program verifications- verification condition
generator
• EBS, Chen, Yeh, Reed et al
• Concurrent programs, Hailpern,Owicki, Lamport and
Schneider
General discussion
• Abstract logic component decomposition verification and
efficiency analysis
• Practical tools, such as UML