2,327 research outputs found
Relative Liveness and Behavior Abstraction (extended abstract)
No full textion (Extended Abstract) Ulrich Nitsche University of Zurich, Department of Computer Science Winterthurerstr. 190, CH-8057 Zurich, Switzerland Email: [email protected] Pierre Wolper University of Li`ege, Institute Montefiore, B28 B-4000 Li`ege Sart Tilman, Belgium Email: [email protected] Abstract This paper is motivated by the fact that verifying liveness properties under a fairness condition is often problematic, especially when abstraction is used. It shows that using a more abstract notion than truth under fairness, specifically the concept of relative liveness property can lead to interesting possibilities. Technically, it is first established that deciding relative liveness is a PSPACE-complete problem and it is shown that relative liveness properties can always be satisfied by some fair implementation. Thereafter, the interaction between behavior abstraction and relative liveness properties is studied and it is proved that relative liveness properties can be verifie..
Do We Need Liveness? Approximation of Liveness Properties by Safety Properties
No full textWe explore in this paper the approximation of a liveness property by a safety property (with respect to a given system behaviour). The approximation is such that, if a system satisfies only the approximation of a linear-time property but not the property itself, we will only detect this by observing the system for an infinite time. As an infinitely long observation is practically impossible, we must deem the property to hold as soon as its approximation is satisfied
Secure Server-Side Java Applications
No full textJava Servlets offer a convenient way to implement Java programs that run on the server side. Being exposed to public access via the Internet, they are equipped with security mechanisms to protect the Internet server from various types of threats. I will discuss in this article the security features provided by Java Servlets. In addition, I will describe briefly the additional mechanisms that need to be put into place to create secure server-side Internet applications
Satisfaction up to Liveness ? Automatic Verification based on Exhaustive Testing
No full textAn approximation to the usual linear satisfaction of temporal properties is discussed in this paper. It is called satisfaction up to liveness as it only differs from the linear satisfaction relation on liveness but not on safety properties. From the point of view of observation, satisfaction up to liveness and linear satisfaction are indistinguishable. Roughly speaking, by observing all finite behaviours (exhaustive testing), we do not know whether a system satisfies a property up to liveness or linearly. Being indistinguishable from linear satisfaction in terms of complete observations, satisfaction up to liveness offers an alternative approach to model-checking
Checking Properties within Fairness and Behavior Abstraction
No full textThis paper is motivated by the fact that verifying liveness properties under a fairness condition is often problematic, especially when abstraction is used. It shows that using a more abstract notion than truth under fairness, specifically the concept of a property being satisfied within fairness can lead to interesting possibilities. Technically, it is first established that deciding satisfaction within fairness is a PSPACE-complete problem and it is shown that properties satisfied within fairness can always be satisfied by some fair implementation. Thereafter, the interaction between behavior abstraction and satisfaction within fairness is studied and it is proved that satisfaction of properties within fairness can be verified on behavior abstractions, if the abstraction homomorphism is weakly continuation-closed
Computing Property-Preserving Behaviour Abstractions from Trace Reductions
No full textWeakly continuation-closed abstractions are known to preserve properties satisfied within fairness, i.e. linear-time temporal properties under an abstract notion of fairness. Being defined on the complete behaviour of a distributed system, weakly continuation-closed abstractions require, in principle, an exhaustive state-space construction prior to abstraction. Constructing the state-space of a practically relevant specification exhaustively, however, is usually unfeasible. Based on the notion of traces, i.e. certain equivalence classes of behaviours, we define trace reductions. Trace reductions are a particular partial-order reduction based on the persistent-set selective search technique. We show that a trace reduction can be used on behalf of the complete behaviour of a distributed system in order to compute abstractions as well as to check whether the abstractions are weakly continuation-closed. Thus, trace reductions allow us to overcome the requirement of an exhaustive state-space construction prior to abstraction
Secure Internet-Access to Medical Data
No full textThe concept of context-dependent access control has emerged during the last years: Information about the state of a process model of a working environment is combined with general knowledge about a person to grant or revoke access to protected data. Being understood very well in principle, different problems arise when implementing context-dependent access control, in particular on an open network. This paper reports on context-dependent access control to support distributed clinical trials. Centrally stored data will be accessed from contributors to a clinical trial over the Internet. We present in this paper how context-dependent access control can be implemented on the Internet in a secure way, using Java Servlets to implement the access control and SSL to secure communication. Keywords: Workflow-support for clinical trials, telemedicine, context-dependent access controls, health information systems
- …
