Search

Real-time software is usually used in circumstances where safety is important and the margin for errors is narrow. These kinds of systems have applicability in a broad band of domains as: automotive, avionics, air traffic control, nuclear power stations, industrial control, etc. As the name denotes, the main feature of "real-time" applications is the criticality of their timeliness. Guaranteeing certain timeliness requires appropriate testing. As manual testing is burdensome and error prone, automated testing techniques are required. Although the importance of having a standard environment for automatic testing is high, the technologies in this area are not sufficiently developed. This paper reviews the standardized test description language "Testing and Test Control Notation version 3 (TTCN-3)" as a mean for real-time testing and proposes extensions to enable real-time testing with TTCN-3. The aim is to provide a complete testing solution for automatic functional and real-time testing, built around this already standardized testing language. The solution includes an environment for designing and running the tests written in the extended language. As a proof of concept, test examples, designed using the enhanced TTCN-3, are mapped to real-time platform implementations and the timeliness of each implementation is analyzed.

The re:innovate track highlights different perspectives on Open Innovation. This session presents challenges of the public administration for the civil society. Open Cities "Open Innovation Mechanisms in Smart Cities (Open Cities)" started as EU funded project in the end of 2010. Within the project the participating administrations, research institutions and companies support Open Government activities. The partners from the European major cities Helsinki, Berlin, Amsterdam, Paris, Rome, Barcelona and Bologna transfer methods of Open Innovation -- like Crowdsourcing, Open Data, Fibre to the Home and Open Sensor Networks -- to the public sector and validate the success of the methodologies within pilot projects. Open Cities App Challenge -- Prof. Dr. Ina Schieferdecker Within the scope of the Pan-Europian "Open Cities"-project the Berlin Senate Administration for Economics, Technology and Research supports the open call for the Open Cities App Challenge. This call is directed to all developers and organizations with innovative products or services that uses open data (from the Open Cities open data platform or the Open Cities open sensor platform or any other open data source) and solves a real problem in citizens' every day urban life. Prof. Dr. Ina Schieferdecker presents the challenge, informs about the terms and conditions and calls on to every interested developer to contribute. For further informations check here or the portal. Open Cities Crowdsourcing Challenge -- Esteve Almirall The second Open Cities Challenge that adresses the European audience targets developers and everybody who is interested or engaged in the field of Open Data. Open Cities asks them for their proposals on what kind of data the developers and interested activists would like to see released. This is something that has not been done before and aims to increase the attention and awareness for opening public data. Prof. Esteve Almirall from Barcelona will announce the challenge and presents background, terms and conditions of that call.

Das UML Testing Profile [UTP] ist eine grafische Modellierungssprache zur Definition, Dokumentation, Visualisierung, Implementierung und zum Austausch von modellbasierten Testspezifikationen auf Basis der UML [UML]. Der normative Teil der Spezifikation definiert das native UML-Profil des UTP1. Die Spezifikation des UTP als UML-Profil ist im Vergleich zu anderen Sprachen der UML-Familie [SysML, MARTE, SoaML] deutlich schlanker und kompakter, erfordert aber gleichzeitig profundes UML-Wissen, um die Potenziale von UTP voll ausschöpfen zu können. Ein Umstand, der die Akzeptanz des UTP bis heute behindert, da nur wenige Tester in den Konzepten der Modellierung im Allgemeinen ausreichend geschult und mit der UML im Besonderen vertraut sind. Dieser Artikel widmet sich daher neben einer kurzen Einführung in das UTP vor allem Fragen seiner Anwendbarkeit. Dabei stehen weniger spezifische Domänen, sondern eher grundsätzliche, testmodellspezifische Fragestellungen im Vordergrund.

Wireless nodes equipped with multiple radio interfaces open up new fields of application. Ranging from multi-channel usage in a cell in order to increase the bandwidth to the creation of meshed multi-hop topologies. Using multiple wireless cards demands a large physical space, more energy consumption and as a consequence decreasing in the battery lifetime. Virtualization of the wireless network interface, which means to use a single wireless network interface to connect to more than one network simultaneously, seems to be a promising approach, since it allows us to realize the mentioned scenarios only with one radio interface. In this paper, we want to shed light on the state of the art and want to introduce new approaches to push this field beyond the current status., Electronic Communications of the EASST, Volume 17: Kommunikation in Verteilten Systemen 2009

In requirements engineering, there are several approaches for requirements modeling such as goal-oriented, aspect-driven, and system requirements modeling. In practice, companies often customize a given approach to their specific needs. Thus, we seek a solution that allows customization in a systematic way. In this paper, we propose a metamodel for requirements models (called core metamodel) and an approach for customizing this metamodel in order to support various requirements modeling approaches. The core metamodel represents the common concepts extracted from some prevalent approaches. We define the semantics of the concepts and the relations in the core metamodel. Based on this formalization, we can perform reasoning on requirements that may detect implicit relations and inconsistencies. Our approach for customization keeps the semantics of the core concepts intact and thus allows reuse of tools and reasoning over the customized metamodel. We illustrate the customization of our core metamodel with SysML concepts. As a case study, we apply the reasoning on requirements of an industrial mobile service application based on this customized core requirements metamodel.

This paper reports on the results of the application of formal methods in the development of an industrial, mission-critical system, called the Operator Support System. A critical communication protocol of this system, the OM/RR Protocol, and its corresponding service were formalised using the formal specification language Lotos. The resulting specifications have been validated using the tool set Lite and models of the specifications, obtained by making abstractions, have been verified using the tool Eucalyptus. Whereas the use of formal methods is usually motivated by their ability to allow for unambiguous and precise system descriptions amenable to mathematical reasoning, it turned out that in this project most benefits were obtained by the sheer process of formalising the informal protocol description, revealing many omissions and ambiguities. The results and experiences obtained during formalisation, validation, abstraction and verification are discussed on a non-formal basis in this paper.

Continuous-time Markov chains (CTMCs) are widely used to describe stochastic phenomena in many diverse areas. They are used to estimate performance and reliability characteristics of various nature, for instance to quantify throughputs of manufacturing systems, to locate bottlenecks in communication systems, or to estimate reliability in aerospace systems. CTMCs are the underlying semantic model of major high level performance modelling formalisms such as stochastic Petri nets, stochastic process algebras, and Markovian queueing networks. Model checking is a very successful technique to establish correctness of systems from very similar application domains, usually described in terms of a nondeterministic finite-state model. One of the major reasons for the success of model checking tools in practice is the efficient way to cope with the state-space explosion problem, using symbolic (BDD-based) techniques. In this talk, I will introduce CTMCs and discuss the use of model checking to assess performance and reliability properties of CTMCs. With this approach, properties-of-interest are expressed as formulas of a stochastic extension of the logic CTL and interpreted over CTMCs. Model checking this logic requires the solution of linear systems of equations and of systems of Volterra integral equations. I will outline approximate techniques for solving the equation systems, and present a JAVA implementation of a Markov chain model checker. My introduction to CTMC model checking will be complemented with a discussion of CTMC model construction techniques. I will survey formal methods that facilitate the construction of large CTMC models. In particular I will focus on high-level formalisms supporting a modern, hierarchical and compositional design methodology. Existing tool support, as well as techniques to combat the state space explosion problem will be discussed.