Browsing by Author "Moszkowski, B. C."
Now showing 1 - 19 of 19
Results Per Page
Sort Options
Item Metadata only Automated Test Code Generation Based on Formalized Natural Language Business Rules(International Academy, Research and Industry Association (IARIA), 2012-11) Bacherler, Christian; Moszkowski, B. C.; Facchi, Christian; Huebner, AndreasThe paper addresses two fundamental problems in requirements engineering. The first one is the conflict between understandability for non-programmers and a semantically well-founded representation of business rules. The second one is the verification of productive code against business rules in requirements documents. As a solution, a language to specify business rules that are close to natural language and at the same time formal enough to be processed by computers is introduced. For more domain specific expressiveness, the language framework permits customizing basic language statements, so called atomic formulas. Each atomic formula has a precise semantics by means of predicate and Interval Temporal Logic. The customization feature is demonstrated by an example from the logistics domain. Behavioral business rule statements are specified for this domain and automatically translated to an executable representation of Interval Temporal Logic. Subsequently, the example is utilized to illustrate the verification of requirements by automated test generation based on our formalized natural language business rules. Thus, our framework contributes to an integrated software development process by providing the mechanisms for a human and machine readable specification of business rules and for a direct reuse of such formalized business rules for test-cases.Item Metadata only A complete axiom system for propositional interval temporal logic with infinite time(Tech Univ Braunschweigb, 2012-08) Moszkowski, B. C.Interval Temporal Logic (ITL) is an established temporal formalism for reasoning about time periods. For over 25 years, it has been applied in a number of ways and several ITL variants, axiom systems and tools have been investigated. We solve the longstanding open problem of finding a complete axiom system for basic quantifier-free propositional ITL (PITL) with infinite time for analysing nonterminating computational systems. Our completeness proof uses a reduction to completeness for PITL with finite time and conventional propositional linear-time temporal logic. Unlike completeness proofs of equally expressive logics with nonelementary computational complexity, our semantic approach does not use tableaux, subformula closures or explicit deductions involving encodings of omega automata and nontrivial techniques for complementing them. We believe that our result also provides evidence of the naturalness of interval-based reasoning.Item Metadata only A compositional framework for hardware/software co-design(Springer Verlag, 2002-01-01) Zedan, Hussein; Cau, A. (Antonio); Dimitrov, J.; Hale, R.; Moszkowski, B. C.; Manjunathaiah, M.; Spivey, M.Item Open Access Compositional modelling: The formal perspective(2005-09-05T17:39:33Z) Zedan, Hussein; Cau, A. (Antonio); Moszkowski, B. C.We provide a formal framework within which an Information System (IS) could be modelled, analysed, and verified in a compositional manner. Our work is based on Interval Temporal Logic (ITL) and its programming language subset, Tempura. This is achieved by considering IS, of an enterprise, as a class of reactive systems in which it is continually reacting to asynchronously occurring events within a given period of time. Such a reactive nature permits an enterprise to pursue its business activities to best compete with others in the market place. The technique is illustrated by applying it to a small case study from Public Service Systems (PSS).Item Metadata only Compositional reasoning using intervals and time reversal(IEEE Computer Society, 2011-09-12) Moszkowski, B. C.We apply Interval Temporal Logic (ITL), an established temporal formalism for reasoning about time periods, to extending known facts by looking at them in reverse and then reducing reasoning about infinite time to finite time. Time reversal then helps to compositionally analyse some aspects of concurrent behaviour involving mutual exclusion.Item Metadata only Compositional reasoning using intervals and time reversal(Springer, 2013-06-05) Moszkowski, B. C.Interval Temporal Logic (ITL) is an established formalism for reasoning about time periods. We investigate some simple kinds of ITL formulas which have application to compositional reasoning and furthermore are closed under conjunction and the conventional temporal operator known both as “box” and “always”. Such closures help us modularly construct formulas from simple building blocks in a way which preserves useful compositional properties. The most important class considered here is called the 2-to-1 formulas. They offer an attractive framework for analysing sequential composition in ITL and provide the formal basis for most of the subsequent presentation. A key contribution of this work concerns a useful and apparently new and quite elementary mathematical theorem that 2-to-1 formulas are closed under “box”. We also use a natural form of time symmetry with 2-to-1 formulas. This extends known facts about such formulas by looking at them in reverse. An important example involves showing that 2-to-1 formulas are also closed under a variant of “box” for prefix subintervals rather than suffix ones. We then apply the compositional formulas obtained with time symmetry to analyse concurrent behaviour involving mutual exclusion in both Peterson’s algorithm and a new and more abstract one. At present, our study of mutual exclusion mainly serves as a kind of experimental “proof of concept” and research tool to develop and illustrate some of the logical framework’s promising features. We also discuss how time symmetry sometimes assists in reducing reasoning in ITL to conventional linear-time temporal logic.Item Metadata only Formalising of transactional memory using interval temporal logic (ITL)(IEEE, 2012) El-kustaban, Amin Mohammed Ahmed; Moszkowski, B. C.; Cau, A. (Antonio)Item Metadata only Guest editors' preface to special issue on interval temporal logics(Springer, 2014-04-10) Moszkowski, B. C.; Guelev, D.; Leucker, M.Item Metadata only A hierarchical analysis of propositional temporal logic based on intervals(College Publications, 2005) Moszkowski, B. C.Item Metadata only A hierarchical completeness proof for propositional Interval Temporal Logic with finite time(Springer Verlag, 2004-05-01) Moszkowski, B. C.Item Metadata only A hierarchical completeness proof for propositional temporal logic(Springer Verlag, 2004-02-24) Moszkowski, B. C.Item Metadata only Interconnections between classes of sequentially compositional temporal formulas(Elsevier, 2013) Moszkowski, B. C.Interval Temporal Logic (ITL) is an established formalism for reasoning about time periods. We elucidate here the relationship between various kinds of compositional propositional ITL formulas. Several are closed under conjunction and the standard temporal operator known as “box” and “always".Item Open Access Proving the correctness of the interlock mechanism in processor design.(Chapman & Hall on behalf of the International Federation for Information Processing (IFIP), 1997) Li, Xiaoshan; Cau, A. (Antonio); Moszkowski, B. C.; Coleman, Nick; Zedan, HusseinIn this paper, Interval Temporal Logic (ITL) us used to specify and verify the event processor EP/3, which is a multi-threaded pipeline processor capable of executing parallel programs. We first give the high level specification of the EP/3 with emphasis on the interlock mechanism. The interlock mechanism is used in processor design especially for dealing with pipeline conflict problems. We prove that the specification satisfies certain safety and liveness properties. An advantage of ITL is that it has an executable part, i.e., we can simulate a specification before proving properties about it. This will help us to get the right specification.Item Metadata only Specification analysis of transactional memory using ITL and AnaTempura(2012) El-kustaban, Amin Mohammed Ahmed; Moszkowski, B. C.; Cau, A. (Antonio)Item Metadata only Supporting Test Code Generation with an Easy to Understand Business Rule Language(International Academy, Research and Industry Association (IARIA), 2013-07) Bacherler, Christian; Moszkowski, B. C.; Facchi, ChristianThe paper addresses two fundamental problems in requirements engineering: The first one is the conflict between understandability for non-programmers and a semantically well-founded representation of business rules. The second one is the verification of productive code against business rules in requirements documents. As a solution, a language to specify business rules that are close to natural language and at the same time formal enough to be processed by computers is introduced. A case study with 30 test persons indicates that the proposed language caters to a better understandability for domain experts. For more domain specific expressiveness, the language framework permits the definition of basic language statements. The language also defines business rules as atomic formulas, that are frequently used in practice. This kind of constraints is also called common constraints. Each atomic formula has a precise semantics by means of predicate or Interval Temporal Logic. The customization feature is demonstrated by an example from the logistics domain. Behavioral business rule statements are specified for this domain and automatically translated to an executable representation of Interval Temporal Logic. Subsequently, the verification of requirements by automated test generation is shown. Thus, our framework contributes to an integrated software development process by providing the mechanisms for a human and machine readable specification of business rules and for a direct reuse of such formalized business rules for test cases.Item Open Access Using ITL and Tempura for large scale specification and simulation.(IEEE, 1996) Cau, A. (Antonio); Zedan, Hussein; Coleman, Nick; Moszkowski, B. C.ITL and Tempura are used for respectively the formal specification and simulation of a large scale system, namely the general purpose multi-threaded dataflow processor EP/3. This paper shows that this processor can be specified concisely within ITL and simulated with Tempura. But it also discusses some problems encountered during the specification and simulation, and indicates what should be added to solve those problems.Item Open Access Using PVS for Interval Temporal Logic proofs, part 1: The syntactic and semantic encoding(2005-05-23T20:41:26Z) Cau, A. (Antonio); Moszkowski, B. C.Interval temporal logic (ITL) is a logic that is used to specify and reason about systems. The logic has a powerful proof system but rather than doing proofs by hand, which is tedious and error prone, we want a tool that can check each proof step. Instead of developing a new tool we will use the existing prototype verification system (PVS) as a basic tool. The specification language of PVS is used to encode interval temporal logic semantically and syntactically. With this we can encode the ITL proof system within PVS. Several examples of proofs in ITL that are done per hand are checked with PVS.Item Metadata only Using temporal logic to analyse temporal logic: A hierarchical approach based on intervals(Oxford University Press, 2007-04-01) Moszkowski, B. C.Item Metadata only Verification and enforcement of access control policies(Springer, 2013) Cau, A. (Antonio); Janicke, Helge; Moszkowski, B. C.