140 research outputs found
Invited Talk Beyond Single Cluster Reachability Analysis
No full textColloquium on Automata, Languages and Programming (ICALP 2005). The primary mission was to present recent developments in this new research domain and additionally building and strengthening the relationship between people working in the area of parallel and distributed approaches to the verification of large-scale systems. The workshop program included an invited talk by Gerd Behrmann & Kim G. Larsen on “Beyond Single Cluster Reachability Analysis”. Besides regular papers, short presentations describing “work in progress” were accepted to strengthen the workshop atmosphere. In total, 5 regular papers and 4 short presentations have been accepted by the following program committee
Martin Behrmann\u27s Lehrbuch Fuer Chorleitung: a Translation. (Volumes One and Two).
No full textMartin Behrmann is the Director of the Berliner Kirchenmusik- schule in the Spandau section of West Berlin. Behrmann is also the conductor of the Spandauer Kantorei and another civic chorus in Hamburg, West Germany. Lehrbuch fur Chorleitung is the first of three volumes to be pub- lished by Hannsler-Verlag of Stuttgart. This first volume is due to be released by the publisher in the summer of 1985. Behrmann assumes and defends the position that conducting does not require special talent. The author maintains that conduc- ting can be taught and then proceeds to demonstrate his method. This method consists primarily of stimulating every conceivable musical problem which a choral conductor might encounter and rehearsing it with the assistance of an instructor. Behrmann places particular emphasis on rehearsal technique, advocating his own technique as one which can be studied in order for a beginner conductor to be able to develop his own individual technique. The author divides rehearsals into four phases and describes each phase, the duration, the material to be addressed, and the results to be expected. Within these four phases, difficulties are placed into three classifications. The majority of the book addresses these classifications of difficulties and all that they entail. Numerous excerpts from compositions (mostly by German composers) as well as short exercises by Behrmann are utilized throughout the book. The final chapter is demonstrative, more specifically, of his rehearsal technique concerning one particular piece of music, Wie der Hirschshreiet by Distler
Resource-optimal scheduling using priced timed automata
No full textThis contribution reports on the considerable effort made recently towards extending and applying well-established timed automata technology to optimal scheduling and planning problems. The effort of the authors in this direction has to a large extent been carried out as part of the European projects VHS (VHS 2005) and AMETIST (AMETIST 2005) and are available in the recently released UPPAAL CORA (UPPAAL CORA 2005), a variant of the real-time verification tool UP-PAAL (Larsen, Pettersson, & Yi 1997; Behrmann, David, & Larsen 2004) specialized for cost-optimal reachability for the extended model of so-called priced timed automata
New ideas of feminity and a problematical drug consumption concerning adolescent girls
No full textThis dissertation analyses different functions of drugs exoneration for divers groupings of adolescent girls. They locate their identity today in an area of tension between mostly traditional education as an idea of modernity as active an indipendent young women: being a housewife and mother and a career woman at the same time. The question answered in this study is to examine more closely the backgrounds, that induce girls to choose drug consumption as an appropriate coverage strategy for certain task in their personal developement.Middle class girls have so been proved as specificaly affected
A Performance Study of Distributed Timed Automata Reachability Analysis
No full textAbstractWe experimentally evaluate an existing distributed reachability algorithm for timed automata on a Linux Beowulf cluster. It is discovered that the algorithm suffers from load balancing problems and a high communication overhead. The load balancing problems are caused by inclusion checking performed between symbolic states unique to the timed automaton reachability algorithm. We propose adding a proportional load balancing controller on top of the algorithm. We evaluate various approaches to reduce communication overhead by increasing locality and reducing the number of messages. Both approaches increase performance but can make load balancing harder and has unwanted side effects that result in an increased workload
TURTLE: Four Weddings and a Tutorial
No full textThe paper discusses an educational case study of protocol modelling in TURTLE, a real-time UML profile supported by the open source toolkit TTool. The method associated with TURTLE is step by step illustrated with the connection set up and handover procedures defined for the Future Air navigation Systems. The paper covers the following methodological stages: requirement modeling, use-case driven and scenario based analysis, object-oriented design and rapid prototyping in Java. Emphasis is laid on the formal verification of analysis and design diagrams
- …
