Formal Methods of Systems Specification Logical Specification of Hard- and Software

  • Published on
    30-Dec-2015

  • View
    13

  • Download
    2

Embed Size (px)

DESCRIPTION

Formal Methods of Systems Specification Logical Specification of Hard- and Software. Prof. Dr. Holger Schlingloff Institut fr Informatik der Humboldt Universitt and Fraunhofer Institut fr Rechnerarchitektur und Softwaretechnik. Recap: Propositional Logic. - PowerPoint PPT Presentation

Transcript

  • Formal Methods of Systems SpecificationLogical Specification of Hard- and SoftwareProf. Dr. Holger SchlingloffInstitut fr Informatik der Humboldt UniversittandFraunhofer Institut fr Rechnerarchitektur und Softwaretechnik

    Slide *H. Schlingloff, Logical Specification

    Recap: Propositional LogicSyntax PL ::= | | (PL PL)SemanticsPropositional Model M: (U,I); Interpretation I: UValidation relation M M p if I(p)=trueM M () if M implies M Validity (), Satifiability (SAT())Calculus axiom schemes: weakening, distribution, excluded middlerule: modus ponens

    Slide *H. Schlingloff, Logical Specification

    Q.: exponential blowup?(rs) = ((rs) (sr))(q(rs)) = ((q(rs)) ((rs)q))= ((q ((rs) (sr))) (((rs) (sr)) q))(p(q(rs))) = (p(q(rs))) ((q(rs))p)= (p((q((rs) (sr))) (((rs) (sr))q))) (((q((rs) (sr))) (((rs) (sr))q))p)

    p (q r) (q s)q (t u)p ((t u) r) ( (t u) s)

    logarithmic reduction by introduction of abbreviations?

    Slide *H. Schlingloff, Logical Specification

    Boolean Quantification

    QPL ::= | | (QPL QPL) | QPL

    intuitively, p (p) means p is hiddenM p if there is an M= (U,I) such that I(q)=I(q) for all qp and M p ((p:=) (p:=))p = p ; p ((p:=) (p:=))

    Slide *H. Schlingloff, Logical Specification

    Conciseness and ComplexityQuantified formulae can be logarithmically more concise = [ ((rs)t) ((rs)t) ((rs)t) ] (p(p ((rs)t)) [ p p p ])

    Quantified formulae can be exponentially harder to analyzeSAT(PL) is NP-hard, SAT(QPL) is PSPACE-hardTo check whether p holds one has to check both alternatives

    Slide *H. Schlingloff, Logical Specification

    Boolean Normal FormsDNF (disjunctive normal form)each formula is equivalent to a disjunction of conjunction of literals e.g. ((p qr) (pqr) (pqr))obtained by truth tableCNF (conjunctive normal form)de Morgan dual of DNFused in PLAs (programmable logic arrays)NAND-, NOR-normal form(p|q)=(pq); p=(p|p); (pq)=(p|q)used for gate arraysAlgebraic normal formXOR of conjunction of (positive) propositionsused in linear feedback shift registers

    Slide *H. Schlingloff, Logical Specification

    next week: tree normal form(ordering of variables)

    Slide *H. Schlingloff, Logical Specification

    Boolean Modelling of Reactive SystemsMany modelling formalisms are being usedTransition systemsParallel and hierarchical transition systems, statechartsShared variables programsUML diagramsAbstract state machines...

    Slide *H. Schlingloff, Logical Specification

    Transition SystemsTransition system TS=(,S, , S0), where is a nonempty finite alphabetS is a nonempty finite set of states S S is the transition relation, andS0 S is the set of initial statessimilar to a nondeterministic finite automaton, with many initial states but without finite statestransition system generates a (finite or infinite) word w0w1w2... iff there are states s0s1s2s3... such that s0 S0 and each (si,wi,si+1)

    Slide *H. Schlingloff, Logical Specification

    Example={up, dn}S={off, tape, memory, play}={(off,dn,tape), (tape,up,off), (tape,dn,memory), (memory,up,off), (memory,dn,play), (play,dn,tape), (play,up,off)}S0={off}

    Slide *H. Schlingloff, Logical Specification

    Parallel Transition SystemsParallel transition system T=(T1,,Tn)each Ti is a transition systemSiSj=interleaving semanticson its private alphabet, each Ti can make an independent movesynchronization is via common eventsexample: power switch and camcorder mode

    Slide *H. Schlingloff, Logical Specification

    ExampleT=(switch, camera){pwr_fail, pwr_res} are private to camerasynchronization alphabet {up,dn}how big is the state space?

    Slide *H. Schlingloff, Logical Specification

    The global transition system T associated with a parallel transition system (T1,,Tn) is defined as T=(, S, , S0), where= iS= S1 SnS0 = S1,0 Sn,0, and((s1,,sn),a,(s1,,sn)) iff for all Tiif ai, then ((s i),a,(s i))i, andif ai, then s i=s i.

    Slide *H. Schlingloff, Logical Specification

    Shared VariablesA shared variables program is given by a tuple (V,D,T,s0), whereV=(v1,,vn) is a set of program variablesD=(D1,,Dn) is a tuple of corresponding finite domains Di={di1,,dim}TDD is a transition relation, ands0 = (d11,,dn1) is the initial state

    Slide *H. Schlingloff, Logical Specification

    Example (1)A request granting algorithmV={request,state}D=({true, false}, {ready, busy})T=(((true, ready), (true, busy)), ((false, ready), (false, ready)), ((true, busy), (true, busy)), ((true, busy), (true, ready)), )

    Slide *H. Schlingloff, Logical Specification

    Example (2)Euclidean algorithm gcd(a, b) if a = 0 return b while b 0 if a > b then a := a b else b := b a return aShared variables programV=(a,b)D=(Nat, Nat) (finite?)T={((0,0),(0,0)), ((7,4),(3,4)), ((3,4),(3,1)), }s0=D

    Slide *H. Schlingloff, Logical Specification

    Transition Systems and ProgramsFor every (parallel) transition system there is an equivalent shared variables program of the same order of size.The translation in the other direction may cause an exponential blowup.Exercise: describe the translations! In which sense are the translations equivalent?

    Slide *H. Schlingloff, Logical Specification

    Transition Relation as Boolean FormulaState=(d1,,dn) (diDi)Transition relation T can be defined by a propositional formula Tatomic propositions: let V={v1,,vn} P={(x=y) | x,y (VVDi)}Any propositional formula T in this alphabet defines a transition relation via the following conventionIf s=(d1,,dn) and s=(d1,dn), then (s,s) T iff M T, where I(vi)=di and I(vi)=di.

    Slide *H. Schlingloff, Logical Specification

    Examplerequest granting algorithmV={request,state}D=({true, false}, {ready, busy})T=((request=true)(state=ready)(state=busy))Propositional logic as a programming languageUsed in model checkers such as nuSMV

Recommended

View more >