Swedish web site
SaS Seminars 2001
Software and Systems Research Seminar Series
Fall 2001
NASA Space Robotics: State-of-the-art Assessment and Future Capabilities
Date: December 13 Place: Planck, IFM, Time: 15.15
David Kortenkamp, NASA Johnson Space Center, Houston
Abstract: This talk will present the current state-of-the-art in space robotics. It will cover both robotics for planetary surface exploration and for orbital assembly and maintenance. In addition to presenting the current state-of-the-art the talk will give ten year projections on expected capabilities. These projections are based on discussions with leading robotics researchers. This assessment is driven by a detailed break-down of robotic capabilities that are necessary for space operations. The breakdown includes mobility, sensing, manipulation, planning and execution and human/robot interaction. A series of metrics for each capability are used to assess the state-of-the-art and project progress. The talk will include video of various NASA robotics projects to illustrate current capabilities.
Speaker's bio: David Kortenkamp received his B.S. in computer science from the University of Minnesota in 1988. He received his M.S. and Ph.D. in computer science and engineering from the University of Michigan in 1990 and 1993 respectively. His doctoral thesis described a method for integrating stereo vision and sonar sensing data on-board a mobile robot. While at Michigan, Dr. Kortenkamp led a team of researchers to a first place finish in the 1992 American Association for Artificial Intelligence Mobile Robot Contest. After receiving his doctorate, he began working as a contractor at NASA Johnson Space Center in Houston Texas. Dr. Kortenkamp was chair of the 1999 IJCAI Workshop on Adjustable Autonomy Systems, was on the program committee for AAAI-96, AAAI-97, AAAI-98, AAAI-99 and AAAI-2000 and was the co-organizer of the 1998 AAAI Mobile Robot Contest. He was also guest editor of a special issue of the Journal of Experimental and Theoretical Artificial Intelligence devoted to robot architectures and a guest editor of a special issue of Autonomous Robots. He, along with Pete Bonasso and Robin Murphy, edited the book Artificial Intelligence and Mobile Robots published by MIT Press in 1998. Dr. Kortenkamp serves as associate editor of the MIT Press Series on Intelligent Robotics and Autonomous Agents. He is author or co-author of six journal articles and more than a dozen refereed conference papers.
Multiclock Esterel: An Unified Formalism for Synchrony and Asynchrony
Date: November 22 Place: Estraden, Time: 15.15
R. K. Shyamasundar, School of Technology & Computer Science, Tata Institute of Fundamental Research
Abstract VLSI circuit design has gained considerably from the introduction of hardware description languages (or HDLs). While these languages are well suited to describe circuits in great detail, they are found wanting when attempting formal verification of circuits. VHDL is the de facto standard used in the VLSI industry and given the wide variety of tools that exists to carry out simulations for circuit specifications in VHDL, it behooves one to explore the possibility of interfacing it with synchronous programming languages to handle higher levels of abstraction in circuit design.
In this talk, we show how the paradigm of multiclock Esterel provides a framework for the design of multi-clocked systems and asynchronous systems. We show how Multi-clock Esterel while preserving the synchrony features embeds Communicating Reactive Processes (CRP) proposed as a formalism for integrating synchrony and asynchrony and provides a unified framework for network of synchronous systems. It can also be used for modelling distributed timed systems. Further, Multiclock Esterel can be used for modelling in conjunction with VHDL to enable formal verification of circuit behaviour. We shall also discuss modelling of VHDL features in multiclock Esterel. Further, we shall also discuss multi-clock formalisms in other synchrnous languages.
Integrated Deductive Software Design with the KeY Tool
Date: October 25 Place: Estraden, Time: 15.15
Reiner Hähnle, Department of Computing Science, Chalmers University of Technology
Speaker's bio: Reiner Hähnle is an associate professor (docent) in computing science and director of graduate studies at the Department of Computing Science, Chalmers University of Technology. He is also a senior consultant for Safelogic AB, Gothenburg. He received a PhD in Computer Science in 1992 from University of Karlsruhe, and the title Universitätsdozent (Habilitation) from Technical University of Vienna in 1997. He joined Chalmers in January 2000. His main research interests are in software verification, automated theorem proving, and non-classical logics. He is currently Chair of the Technical Committee on Multiple-Valued Logic of the IEEE Computer Society and President of the Steering Committee of the TABLEAUX conference.
Abstract: Assessments of the prospects of formal methods in software development widely agree that one can, in principle, increase software quality considerably by using formal methods, but they are considered to be too difficult and expensive to use in industrial practice.
Among the biggest obstacles in the use of formal methods are their lack of integration with CASE tools and the missing support in creating formal specifications of software requirements.
The KeY tool, jointly developed at Chalmers and Karlsruhe University, is based on a commercial UML CASE tool for object-oriented software development in Java. In addition, it features seamless integration of formal specification and verification.
An important aspect is user support for creating formal specifications of requirements. This is illustrated, for example, by our usage of the knowledge embodied in software design patterns: attached to each pattern are properly formalized schmatic properties and requirements that are typically associated with it. When the user selects and applies a pattern from the CASE tool's library, he also obtains suitably instantiated and relevant requirements expressed in the language OCL (Object Constraint Language), which is a subset of the industry standard UML.
Other parts of the project concern generating natural language documents from OCL specifications, a verification system for full sequential Java, and an innovative interactive/automated theorem prover.
In the talk I will first give an outline of the project and tool, and then highlight selected features by example.
Models of Computation in Embedded System Design
Axel Jantsch, Electronic System Design Laboratory, Royal Institute of Technology
Date: September 27, Place: Estraden, Time: 15.15
Speaker's bio: Axel Jantsch received his Master and PhD degrees in computer science from Technical University of Vienna, Austria in 1987 and 1993, respectively. Since 1997 he is associate professor at the Royal Institute of Technology in Stockholm. His current research interests include modeling, design and validation of embedded systems and systems on a single chip.
Abstract: This lecture will present the main models of computation and concurrency, i.e. data flow models, clocked synchronous and perfectly synchronous models, and discrete event models. All these models and many of their variants are used in embedded system design. They are used for different purposes and in different situations. It will be illustrated how these concepts define and limit the potential use of a given language. There is a clear trend today towards the integration of these different computational models and the talsk will summarize the main approaches how this is done and give an outlook on the future developments.
Page responsible: Christoph Kessler
Last updated: 2012-08-17
