<> "The repository administrator has not yet configured an RDF license."^^ . <> . . . "A Pre-processing Tool for Z2SAL to Broaden\r\nSupport 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, Z2SAL, that takes\r\na Z specification and translates it into the input for Symbolic Analysis\r\nLaboratory (SAL), a framework for combining different tools for abstraction, program analysis, theorem proving and model checking. This paper\r\ndiscusses support for model checking Z specifications, in which the capability of Z2SAL is extended. This support includes a translation of a\r\ngeneric constant and a schema calculus definition. Instead of translating\r\nthese aspects of the Z language into the SAL language as Z2SAL does,\r\na Z specification containing these two notations will be pre-processed,\r\nin which a generic constant definition is redefined to an equivalent axiomatic definition and a schema calculus definition is expanded to a new\r\nschema definition. As a result of a successful redefinition or expansion, a\r\nredefined or expanded Z specification is generated, otherwise the original\r\nZ specification is returned. Results show that the large number of our examples can be run successfully by our system. The redefined or expanded\r\nZ specification can be translated later by Z2SAL and the generated SAL\r\nfile can be model checked or simulated by the SAL tool. Results also\r\nshow that Z2SAL can translate outputs of our system to some extent.\r\nThe majority of generated SAL files can be run by the SAL tool."^^ . . "561" . . "Springer International Publishing"^^ . . . . . . . . "Maria Ulfah"^^ . "Siregar"^^ . "Maria Ulfah Siregar"^^ . . . . . . "A Pre-processing Tool for Z2SAL to Broaden\r\nSupport for Model Checking Z Specifications (Text)"^^ . . . . . "PreprocessingToolforZ2SAL.pdf"^^ . . . "A Pre-processing Tool for Z2SAL to Broaden\r\nSupport for Model Checking Z Specifications (Other)"^^ . . . . . . "lightbox.jpg"^^ . . . "A Pre-processing Tool for Z2SAL to Broaden\r\nSupport for Model Checking Z Specifications (Other)"^^ . . . . . . "preview.jpg"^^ . . . "A Pre-processing Tool for Z2SAL to Broaden\r\nSupport for Model Checking Z Specifications (Other)"^^ . . . . . . "medium.jpg"^^ . . . "A Pre-processing Tool for Z2SAL to Broaden\r\nSupport for Model Checking Z Specifications (Other)"^^ . . . . . . "small.jpg"^^ . . "HTML Summary of #39304 \n\nA Pre-processing Tool for Z2SAL to Broaden \nSupport for Model Checking Z Specifications\n\n" . "text/html" . . . "Tehnik Informatika"@en . .