<> "The repository administrator has not yet configured an RDF license."^^ . <> . . . "Support for Model Checking Z Specifications"^^ . "One of the deficiencies of Z tools is that there is limited\r\nsupport for model checking Z specifications. Building a model checker\r\ndirectly for a Z specification will take considerable amount of effort and\r\ntime due to the abstraction of the language. Translating a Z specification input into a specification in a language that an existing model\r\nchecker tool accepts is an alternative method. Researchers at the University of Sheffield implemented a translation tool, which they called\r\nZ2SAL that takes a Z specification and translates it into the input for\r\nSymbolic Analysis Laboratory (SAL), which is a framework for combining different tools for abstraction, program analysis, theorem proving\r\nand model checking. This paper discusses support for model checking Z\r\nspecifications, in which the capability of Z2SAL is extended. This support includes a translation of a generic constant and a schema calculus\r\ndefinition. Instead of translating these aspects of the Z language into\r\nthe SAL language as Z2SAL does, a Z specification containing these two\r\nnotations will be pre-processed, in which a generic constant definition\r\nis redefined to an equivalent axiomatic definition and a schema calculus\r\ndefinition is expanded to a new schema definition. As a result of a successful redefinition or expansion, a redefined or expanded Z specification\r\nis generated, otherwise the Z specification input is returned."^^ . . . . . . . . "Maria Ulfah"^^ . "Siregar"^^ . "Maria Ulfah Siregar"^^ . . . . "FMi 2016 in IRI 2016"^^ . . . . . . "Support for Model Checking Z Specifications (Text)"^^ . . . . . "SupportforModelCheckingZSpec.pdf"^^ . . . "Support for Model Checking Z Specifications (Other)"^^ . . . . . . "lightbox.jpg"^^ . . . "Support for Model Checking Z Specifications (Other)"^^ . . . . . . "preview.jpg"^^ . . . "Support for Model Checking Z Specifications (Other)"^^ . . . . . . "medium.jpg"^^ . . . "Support for Model Checking Z Specifications (Other)"^^ . . . . . . "small.jpg"^^ . . "HTML Summary of #39305 \n\nSupport for Model Checking Z Specifications\n\n" . "text/html" . . . "Tehnik Informatika"@en . .