C. Compositional Design and Verification of Component-Based Information Systems Jan Martijn van der Werf.

  • Published on
    01-Apr-2015

  • View
    213

  • Download
    1

Transcript

<ul><li>Slide 1</li></ul> <p>C. Compositional Design and Verification of Component-Based Information Systems Jan Martijn van der Werf Slide 2 Organizations cooperate Bob Charley Alice Who-knows-who not transitive! Dave Slide 3 Organizations deliver services Bob Charley Alice Dave Slide 4 Component-based information system Process Data Process Data Process Data Process Data Process Data Process Data Slide 5 Verification vs. design Verification: Go and do what you want, check when finished Correctness by design: Follow my rules, and it is correct vs. Slide 6 Compositional verification of soundness Components form a service tree Components only know their direct neighbors B C E D = soundness of component = condition on communicating pair of components A F Slide 7 Compositional verification of soundness Slide 8 Soundness not sufficient for pairwise verification! Slide 9 Compositional design: refinement rules! Stepwise refinement Each step preserves soundness Refinement rules: Within component Outsourcing Over components Slide 10 Process + Data = Prototype + + Slide 11 Compositional design and verification of Component-based information systems Framework for component-based information systems Compositional verification of interaction Compositional design of interaction Petri nets extended with data Message passing Data transactions Process + data prototype Re-engineering by process mining Slide 12 C Compositional Design and Verification of Component-Based Information Systems Jan Martijn van der Werf Slide 13 Soundness: always possible to finish properly (disregarding interfaces) Components and their composition a b c d e a b c d e H I GG Slide 14 Correctness by design Refinement within a component Slide 15 Correctness by design Refinement over components Slide 16 Correctness by design Outsource refinement Slide 17 Sufficient conditions for Slide 18 Sufficient conditions for soundness BB+C B B Identical communication: B+C behaves like B on interface with A Alternating communication block: B+C has same communication blocks as B Elastic communication: B+C may send earlier and receive later than B </p>

Recommended

View more >