Formalne metode v programskem inzenirstvu

RV 1.del: TLA

Literatura in povezave

• Wikipedia: Formal verification
• Wikipedia: Model checking
• Wikipedia: Temporal logic of actions

• Leslie Lamport: Specifying Systems, Addison-Wesley Professional, 2002
• TLA+ Tools - download (Javin program, za izvajanje rabi JRE)
• A Summary of TLA+ (na kratko podana sintaksa TLA+)

• MeolicVaja1.tla
• MeolicVaja2.tla
• MeolicVaja3.tla
• MeolicVaja4.tla
• MeolicVaja5.tla
• MeolicVaja6.tla
• MeolicVaja7.tla, MeolicVaja7MC.tla, MeolicVaja7MC.cfg

• Georg Ferdinand Ludwig Phillip Cantor (1845 - 1918)
• Friedrich Ludwig Gottlob Frege (1848 - 1925)
• Bertrand Arthur William Russell (1872 - 1970)
• Alfred Tarski (1901 - 1983)
• Kurt Gödel (1906 - 1978)
• Raymond Merrill Smullyan (1919)

• Edsger Wybe Dijkstra (1930 - 2002)
• Charles Antony Richard Hoare (1934)
• Arthur John Robin Gorell Milner (1934)
• Leslie Lamport (1941)
• Edmund Melson Clarke, Jr. (1945)

RV 2.del: UML

Literatura in povezave

• Wikipedia: Unified Modeling Language in Object Constraint Language
• Wikipedia: Unified Process
• Wikipedia: IBM Rational Unified Process
• Wikipedia: Agile Unified Process
• Wikipedia: Essential Unified Process

• Jim Arlow, Ila Neustadt: UML 2 and the Unified Process: Practical Object-Oriented Analysis and Design, knjiga, 2005, BookDepository, Amazon.de, Amazon.co.uk
• Miro Samek: Practical UML Statecharts in C/C++: Event-Driven Programming for Embedded Systems, knjiga, 2008, BookDepository, Amazon.de, Amazon.co.uk

• The Object Management Group (OMG)
• Tutorials Point: UML Tutorial
• uml-diagrams.org
• Ivar Jacobson International (blog enega od avtorjev UML-ja)

• IBM Rational Tau (prej Telelogic Tau) in IBM Rational Rose Modeler
• Visual Paradigm for UML (priporocljivo, studenti UM imajo dovoljenje za prosto uporabo!)
• Astah (priporocljivo!)
• UML Lab for Eclipse (priporocljivo!)
• MagicDraw
• Enterprise Architect
• Borland Together
• Altova UModel
• Metamill
• Poseidon for UML
• SinelaboreRT
• Cadifra UML Editor
• UMLStudio
• BOUML

Prosta orodja

• yUML (priporocljivo!)
• Modelio
• Umbrello UML Modeller
• Astade
• Dia + Dia2Code + AutoDia
• ArgoUML
• Oracle JDeveloper
• Papyrus for Eclipse
• Violet UML editor
• Gaphor
• UMLet
• StarUML
• Open ModelSphere
• NClass

Ucno gradivo

• useCase.pdf
• class.pdf
• kupiKavo.pdf
• kupiCaj.pdf
• kuhanjeCaja.pdf
• krmilnik.pdf
• kuhalnik.pdf
• trace.pdf

Zanimivi posamezniki

• Noam Chomsky (1928)
• Barry Boehm (1935)
• David Harel (1950)

• Ivar Jacobson (1939)
• James Rumbaugh (1947)
• Grady Booch (1955)

RV 3.del: SDL in MSC

Literatura in povezave

• Wikipedia: Specification and Description Language
• Wikipedia: Message Sequence Chart

• IBM Rational SDL Suite (prej Telelogic SDL Suite) - dokumentacija za SDL Suite (uporabni dokumenti so Getting Started Guide, Methodology Guide in User Manual)
• V industriji (npr. Iskratel) se ze vrsto let uporablja orodje ObjectGEODE, ki ga je razvilo francosko podjetje Verilog. Tega podjetja danes vec ni in tudi orodje se ne razvija vec.
• SDL Forum Society

• gradivo-sdl.pdf

Zanimivi posamezniki

• Ana Robnik