Browsing by Author "Cau, A. (Antonio)"
Now showing items 1-20 of 44
-
ATOM: an object-based formal method for real-time systems
Zedan, Hussein; Cau, A. (Antonio); Chen, Zhiqiang; Yang, Hongji (Article)An object based formal method for the development of real-time systems, called ATOM, is presented. The method is an integration of the real-time formal technique TAM (Temporal Agent Model) with an industry-strength structured ... -
Behavioural API based Virus Analysis and Detection
Al Amro, S.; Cau, A. (Antonio) (Article)The growing number of computer viruses and the detection of zero day malware have been the concern for security researchers for a large period of time. Existing antivirus products (AVs) rely on detecting virus signatures ... -
The Calculus of context-aware ambients.
Siewe, Francois; Zedan, Hussein; Cau, A. (Antonio) (Article)We present the Calculus of Context-aware Ambients (CCA in short) for the modelling and verification of mobile systems that are context-aware. This process calculus is built upon the calculus of mobile ambients and introduces ... -
CCA: a calculus of context-aware ambients.
Siewe, Francois; Cau, A. (Antonio); Zedan, Hussein (Conference)We present a process calculus, CCA, for the modelling and verification of mobile systems that are context-aware. This process calculus is built upon the calculus of mobile ambients and introduces new constructs to enable ... -
Compositional modelling: The formal perspective
Zedan, Hussein; Cau, A. (Antonio); Moszkowski, B. C. (Article)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 ... -
Compositional verification and specification of refinement for reactive systems in a dense time temporal logic
Cau, A. (Antonio) (Thesis)This thesis introduces a compostitional dense time temporal logic for the compositions and refinement of reactive systems. A reactive system is specified by a pair consisting of a machine and a condition on the computations ... -
A dense-time temporal logic with nice compositionality properties
Cau, A. (Antonio); de Roever, W. P. (Article)A dense temporal logic specification method for the development of reactive systems is introduced. The two development constructs of this method are refinement and composition. A reactive system is specified by a pair ... -
Designing a provably correct robot control system using a "lean" formal method
Cau, A. (Antonio); Czarnecki, Christopher Antoni; Zedan, Hussein (Book chapter)A development method for the construction of provably correct robot control systems together with its supporting tool environment are described. The method consists of four stages: 1. specification, 2. refinement, 3. ... -
Dynamic Access Control Policies - Specification and Verification
Janicke, Helge; Cau, A. (Antonio); Siewe, Francois; Zedan, Hussein (Article)Security requirements deal with the protection of assets against unauthorized access (disclosure or modification) and their availability to authorized users. Temporal constraints of history-based access control policies ... -
A Formal design technique for real-time embedded systems development using duration calculus.
Siewe, Francois; Hung, D. V.; Zedan, Hussein; Cau, A. (Antonio) (Conference)In this paper we present a syntactical approach for the design of real-time embedded systems. The require- ment of the system is specified as Duration Calculus formula over continuous state variables. We model discretization ...