004 Datenverarbeitung; Informatik
Refine
Year of publication
- 2010 (2) (remove)
Document Type
- Doctoral Thesis (2) (remove)
Keywords
- IM-Systeme (1)
- Instant Messaging (1)
- Multiagentensysteme (1)
- hybrid automata (1)
- hybride Automaten (1)
- multiagent systems (1)
Institute
Specifying behaviors of multi-agent systems (MASs) is a demanding task, especially when applied in safety-critical systems. In the latter systems, the specification of behaviors has to be carried out carefully in order to avoid side effects that might cause unwanted or even disastrous behaviors. Thus, formal methods based on mathematical models of the system under design are helpful. They not only allow us to formally specify the system at different levels of abstraction, but also to verify the consistency of the specified systems before implementing them. The formal specification aims a precise and unambiguous description of the behavior of MASs, whereas the verification aims at proving the satisfaction of specified requirements. A behavior of an agent can be described as discrete changes of its states with respect to external or internal actions. Whenever an action occurs, the agent moves from one state to another one. Therefore, an efficient way to model this type of discrete behaviors is to use a kind of state transition diagrams such as finite automata. One remarkable advantage of such transition diagrams is that they lend themselves formal analysis techniques using model checking. The latter is an automatic verification technique which determines whether given properties are satisfied within a model underlying a particular system. In realistic physical environments, however, it is necessary to consider continuous behaviors in addition to discrete behaviors of MASs. Examples of those type of behaviors include the movement of a soccer agent to kick off or to go to the ball, the process of putting out the fire by a fire brigade agent in a rescue scenario, or any other behaviors that depend on any timed physical law. The traditional state transition diagrams are not sufficient to combine these types of behaviors. Hybrid automata offer an elegant method to capture such types of behaviors. Hybrid automata extend regular state transition diagrams with methods that deal with those continuous actions such that the state transition diagrams are used to model the discrete changes of behaviors, while differential equations are used to model the continuous changes. The semantics of hybrid automata make them accessible to formal verification by means of model checking. The main goal of this thesis is to approach hybrid automata for specifying and verifying behaviors of MASs. However, specifying and and verifying behaviors of MASs by means of hybrid automata raises several issues that should be considered. These issues include the complexity, modularity, and the expressiveness of MASs' models. This thesis addresses these issues and provides possible solutions to tackle them.
Moderne Instant-Messaging-Systeme als Plattform für sicherheitskritische kollaborative Anwendungen
(2010)
Many Instant Messaging (IM) systems like Skype or Spark offer extended services, e.g., file sharing, VoIP, or shared whiteboard functionality. IM applications are predominantly used for a spontaneous text-based communication for private purposes. In addition, there is a potential to use such applications in a business context. In particular, the discussion in this dissertation shows that IM systems can serve as platforms for secure collaborative applications (e.g., electronic contract negotiation, e-payment or electronic voting). On the one hand, such applications have to deal with many challenges, e.g., time constraints (an "instant" communication is desired), the integration of multiple media channels and the absence of one unifying "sphere of control" covering all participants. On the other hand, instant messaging systems provide many advantages, e.g., (i) a spontaneous and flexible usage, (ii) easy distribution of information to many participants and (iii) the availability of different channels for the tasks at hand. The original intention of these systems (spontaneous free-flowing information exchange), their modular construction, the unsupervised installation and the ability to easily transmit information over a multitude of channels raise many questions and challenges for IT security. For example, one needs to consider how to contain confidential information, how to verify the authenticity of a communication partner, or how to ensure the non-repudiation of statements. This thesis aims to design security mechanisms that allow to use IM systems as a platform for a collaboration that is both (i) spontaneous and flexible as well as (ii) secure, authentic and non-repudiable. Example applications where such collaboration platforms could be used are the electronic negotiation of contracts, electronic payments or electronic voting.