Publications

 Hybrid systems contain both discrete and continuous components, and therefore it is desirable to have a method which decomposes the verification of a hybrid system into verification of its continuous and discrete components. In this paper, the system we consider may have non-trivial discrete components, such as computer algorithms with iteration structures. We take the view that a single discrete action is instantaneous, and a finite number of discrete actions happening at one time point is still instantaneous, but infinitely many discrete actions occurring at one time leads to losing control of the continuous components and this should in general be avoided in a design. We develop a variant of Duration Calculus in which we embed Hoare Logic used to verify discrete components. Several other rules are proposed in the calculus for proving temporal properties. The paper concludes with a simple example.

 We investigate formal derivation of control programs via the case study of a heating system. The requirements are specified using Duration Calculus, a real time interval logic, and the plant is represented as communicating phase transition systems. Afterwards, Duration Calculus and traditional program logic are applied to derive the control algorithm.

 We use a variant of the Duration Calculus to design a chemical concentration control system which has both nontrivial dynamics and control programs. The system is developed by refinement along the lines proposed in formal methods of software construction. Refinement rules for durational specification formulae are investigated for this purpose. The overall specification is refined into several lower level specifications. One such lower level specification is implemented by software and a control program is proposed and shown to be correct.

 Three different styles of refinement of concurrent systems are investigated. The methods differ in their degree of compositionality. The traditional method considers the refinement of complete systems, and therefore is totally noncompositional. The middle level one is called a modular method, with which one first verifies refinement of each component and then checks that the refinements are compatible by an interference freedom test. The last and more novel one, borrows the rely--guarantee idea from program verification and supports compositional refinement in that one can carry out the development of one process without knowing the structure of other processes. A common example is verified by the various refinement methods. We discuss both advantages and disadvantages of the three approaches, which indicate when it is more suitable to use one particular style.

We present a new formal validation method for healthcare security policies in the form of feedback-based queries to ensure an answer to the question of Who is accessing What in Electronic Health Records. To this end, we consider Role Based Access Control (RBAC) that offers the flexibility to specify users, roles, permissions, actions, and the objects to secure. We use the Z Notation for formal specification of RBAC security policies and for queries to review these security policies. To ease the effort in creating the correct specification of the security policies, RBAC-based graphical models (such as SecureUML) are used and automatically translated into the corresponding Z specification. Both the specification of the queries and the specification of the policies are then animated using the Jaza tool to execute queries against the specification. By this it is automatically shown who will access the medical record of a patient and what information will be exposed to a system user.