Background informationMajor Verification TopicsArchitecture VerificationCommon architecture IssuesCommon architecture problemArchitecture RefinementRefinement pattern approachRefinement patternCompleteness assumptionSlide 10ExampleSlide 12Slide 13Slide 14Slide 15Architecture as TheoriesArchitecture stylesTranslation to LogicSlide 19MappingProvingCompositionproblem exampleSpecificationConcurrent System VerificationExternal SpecificationComposite internal specificationComposite module verificationComposite moduleSimple module specification verificationSimple module internal specsSlide 32DiscussionRelated worksGeneral discussionBackground information•Formal verification methods based on theorem proving techniques and model checking–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 cyclesMajor Verification Topics•Specification Verification•Architecture Verification•General practical issuesArchitecture 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 compositionalCommon architecture Issues•From abstract level to concrete level•Simple architecture: box - arrows, representing data component and connections•Large architecture: Hierarchical approachCommon architecture problem•Limited utility of architecture hierarchy results from the current level of informality•Ambiguity in architecture allows unintended interpretations. May cause erroneous interrepretationArchitecture Refinement•From a abstract architecture to a concrete (lower-level) architecture–lead to:•fewer architectural design errors•extensive and systematic reuse of design knowledge and proofsRefinement pattern approach•A pair architecture schemas (homogenous or heterogeneous)•proven to be relatively correct with respect to the given mapping schemaRefinement pattern•Requires a special correctness criterion–a special mapping between architectures–extensive translation:•the representation of components, interfaces, and connections•aggregated, decomposed, or eliminatedCompleteness 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 trueCompleteness 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 patternsExample•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 compositeExamplecharscodeLexical AnalyzerLexical ParserAnalyzer OptimizerCode Generatortoks ast astbindingsLexical ParserAnalyzer OptimizerastFrom simple dataflow to shared syntax tree:Example: abstract sub-architecture to concrete sub-architectureArchitecture as Theories•Architecture Styles–Operations & axioms•Translation to Logic–Patterns logic (theory generation rules)•Mapping–Name mapping–Style mapping–Interpretation mappingArchitecture stylesDataflow 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 ArchitectureM: MODULE [ Pattern of Concrete ArchitectureMapping•Name mapping:–c | m–op | w•Style mapping:–Accepts (_, _) | Gets (_, _)–Connects (_, _, _) | Writes (_,_) ^ Reads(_,_)•Interpretation mapping = name + style mappingProving•Criterion–all intended to do–not intended to doComposition•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 transitiveproblem 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 CSpecification•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 implementationsConcurrent 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 specificationExternal SpecificationExternal 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 environmentComposite internal specificationInternal specification of a composite module associates events described in the external specification of the module with events described in the external specifications of the sub-modules.• 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 channelsComposite module verificationVerification of composite module:1. External behaviors of the sub-modules plus the network and interface links must imply the external behavior of composite module2. Provides and requires of the sub modules and composite module must be mutually supportive and complete.“mutual support: sub module
View Full Document
Unlocking...