This video paper describes the practical outcome of the first milestone of a project aiming at setting up a so-called Hybrid Team that can accomplish a wide variety of different tasks. In general, the aim is to realize and examine the collaboration of augmented humans with autonomous robots, virtual characters and SoftBots (purely software based agents) working together in a Hybrid Team to accomplish common tasks. The accompanying video shows a customized packaging scenario and can be downloaded from http://hysociatea.dfki.de/?p=441.

Collaborations between organizations in the public sector, e.g., fire brigades, polices, military units, is often done via liaison officers. A liaison officer liaises between two organizations by providing a single point of contact and ensuring the efficient communication and coordination of their activities. Usually an organization embeds a liaison officer in another organization to provide face-to-face coordination. Liaison officers demand special requirements to the security mechanism of the IT infrastructure of the organization that act as host for a liaison officer. This holds, in particular, for Disaster Management Information Systems (DMIS). Such systems need, on the one hand, to support various ways of communication in a flexible and ad hoc manner. On the other hand, these systems need to protect, by law, the leakage of sensitive data. In this paper, we present a novel mechanism, based on role-based access control (RBAC), for supporting the flexible and secure information exchange between organizations using liaison officers. Our mechanism enables liaison officers to decide on their own authority which information they wants share with their home organizations while allowing the host organization to limit the access of liaisons officers to their system in a fine-grained manner.

The goal of this workshop is to explore new technologies, underlying principles, and general methodologies for supporting software certificate management. Software certification demonstrates the reliability, safety, or security of software systems in such a way that it can be checked by an independent authority with minimal trust in the techniques and tools used in the certification process itself. It can build on existing validation and verification (V&V) techniques but introduces the notion of explicit software certificates, which contain all the information necessary for an independent assessment of the demonstrated properties. Software certificates support a product-oriented assurance approach, combining different techniques and forms of evidence (e.g., fault trees, "sign-offs", safety cases, formal proofs, ...) and linking them to the details of the underlying software. A software certificate management system provides the infrastructure to create, maintain, and analyze software certificates. It combines functionalities of a database (e.g., storing and retrieving certificates) and a make-tool (e.g., incremental re-certification). It can also maintain links between system artifacts (e.g., design documents, engineering data sets, or programs) and different varieties of certificates, check the validity of certificates, provide access to explicit audit trails, enable browsing of certification histories, and enforce system-wide certification and release policies. It can at any time provide current information about the certification status of each component in the system, check whether certificates have been audited, compute which certificates remain valid after a system modification, or even automatically start an incremental recertification.

Although formal methods have been successfully applied in various industrial applications, their use in software development is still restricted to individual case studies. To overcome this situation we aim at a methodology for an evolutionary formal software development which allows for a stepwise and incremental development process along the line of rapid prototyping. The approach is based on work on a formal management of change for formal developments which is able to maintain proofs when changing specifications.

The use of formal methods in large complex applications implies the need for an evolutionary formal program development in which specification and verification phases are interleaved. Any change of a specification either by adding new parts or by changing erroneous parts affects existing verification work in a subtle way. We present a truth maintenance system for structured specification and verification. It is based on the simple but powerful notion of a development graph as an underlying data structure to represent an actual consistent state of a formal development. Based on this notion we try to minimize the consequences of changes of existing verification work.

In this paper a survey of the VSE system, a CASE-tool for formal software development, is presented. Main emphasis is put on the underlying formal method and tool support, and that in particular from the deductive support perspective. In order to demonstrate its broad range of applicability and to give an impression on how to work with the system we make use of two (commercial) applications taken from the safety and the IT-security domain.