# 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