[RDF data]
Home | All courseInstance
PropertyValue
sisvu:academicYear 2008 (xsd:int)
is sisvu:courseInstanceLecturerOfCourseInstance of <http://kent.zpr.fer.hr:8080/educationalProgram/resource/courseInstanceLecturer/1199/2008/190992>
sisvu:courseInstanceOfCourseInstanceLecturer <http://kent.zpr.fer.hr:8080/educationalProgram/resource/courseInstanceLecturer/1199/2008/190992>
sisvu:description Formal specification and verification. Verification methods: theorem proving and model checking. Theorem proving: goals, automated verification, theorem provers. Model checking: restrictions, authomated verification, tools. Implementation represented by finite state machine. Specification represented by a temporal logic formula. Checking: does model satisfies specification. State-space searching, state explosion problem. Syimbolic verification. Formal verification and testing. Hardware verification. Application of formal methods in telecommunication. (en)
sisvu:description Formalna specifikacija i verifikacija sustava. Pristupi verifikaciji: dokazivanje teorema i provjera modela. Dokazivanje teorema: ciljevi, automatizacija, dokazivači teorema. Provjera modela: ograničenost mogućnosti i primjene, potpuna automatiziranost, alati. Prikaz implementacije u obliku konačnog automata. Prikaz specifikacije korištenjem formula temporalne logike. Provjera: zadovoljava li model karakteristike zadane formulama temporalne logike. Problem pretraživanja prostora stanja i eksplozije broja stanja. Pristupi rješavanju. Simbolička verifikacija. Formalna verifikacija i testiranje. Verifikacija hardvera. Trenutno stanje primjene formalnih metoda. (hr)
is univ-ont:hasManifestation of <http://kent.zpr.fer.hr:8080/educationalProgram/resource/course/1199>
univ-ont:instanceOfCourse <http://kent.zpr.fer.hr:8080/educationalProgram/resource/course/1199>
rdf:type univ-ont:CourseInstance