Theorie, Praxis und Perspektiven der operationsbasierten formalen Schaltungsverifikation

Formale Methoden wenden mathematische Arbeitsweisen – wie Modellbildung oder das Beweisen wesent-licher Eigenschaften solcher Modelle – auf den Entwurf technischer Systeme an. Das Teilgebiet der formalen Verifikation beschäftigt sich mit dem Beweisen von Eigenschaften wichtiger Modelle. Als besonders wichtig gelten Endliche Automaten, denn diese beschreiben das Verhalten von Software- oder Hardwareimplemen-tierungen diskreter Steuerungen und damit von Schlüsselfunktionalität fast aller technischen Systeme.

Einführend wird der Stand der Kunst des Model Checking erläutert. Technischer Kern des Vortrags ist ein wesentlich anwendungsspezifischeres Verfahren, das durch ein VHDL-Programm beschriebenes Verhalten einer digitalen Schaltung lückenlos und automatisch mit einem abstrakten Automaten, einem abstrakten VHDL, vergleicht. Abstraktes VHDL ist eine Feinspezifikation der Schaltung durch ihre Operationen. Operationen formalisieren i.A. kurze Schaltungsaktivitäten wie Lese- oder Schreibzugriffe, Instruktionen oder Arbitrierungs-zyklen. Es wird erläutert, wie abstraktes VHDL erstellt, bezüglich der Grobspezifikation verifiziert, und dann mit dem VHDL automatisch verglichen wird. Dieser Vergleich zeigt Fehler in der Implementierung der Operationen an sowie Diagnosen zu ihrer Behebung. Automatische Überprüfung eines Kriteriums zur vollständigen Erfassung der Schaltungsfunktionalität durch Operationen garantiert Korrektheit des Codes.  

Es folgt eine kurze Darstellung der Anwendungs- und Prozessseite des Themas: Die operationsbasierte formale Schaltungsverifikation wurde in der zentralen Siemensforschung vor fast 20 Jahren konzipiert, bei Siemens, Infineon und weiteren Chipherstellern erprobt und schließlich in dem Spin-Off OneSpin Solutions zur Produkt-reife geführt. Der Ansatz garantierte Korrektheit zahlreicher VHDL-Programme einer Größenordnung von 100000 LoC – ein prominentes Beispiel ist der in der Automobilelektronik weit verbreitete TriCore-Prozessor von Infineon. Obwohl die Verifikationsproduktivität des Ansatzes mit der der simulationsbasierten Verifikation vergleichbar ist und auch „Nichtformalisten“ die Technik erfolgreich erlernen können, hat sich der Ansatz noch nicht in der Breite durchgesetzt. Auch die Übertragbarkeit des Erfolgsrezepts der operationsbasierten Modellierung auf andere Anwendungsbereiche wie die Fertigungstechnik wurde bisher kaum untersucht.

Der Vortrag schließt mit der Analyse der Erfolgsfaktoren für den Breiteneinsatz der operationsbasierten Schal-tungsverifikation und schildert mögliche nächste Schritte. Vielversprechend erscheint eine weitere Nutzung von abstraktem VHDL für die funktionale Sicherheitsanalyse einer Schaltung. Während Verifikation Entwurfs-fehler aufspürt, beschäftigt sich die Sicherheitsanalyse mit zufälligen Fehlern, verursacht etwa durch Alterungs-prozesse oder durch Strahlungseinflüsse, und so möglichen schwerwiegenden Systemausfällen. Es wird skizziert, wie mithilfe des abstrakten VHDL eine Sicherheitsanalyse für Schaltungen konzipiert und so eine Brücke zwischen formaler Verifikation und funktionaler Sicherheitsanalyse geschlagen wurde.

Kurz-Bio: Wolfram Büttner promovierte 1978 in Mathematik an der Tulane University in New Orleans, habilitierte in diesem Fach an der TU Darmstadt und wechselte dann in die Informatik. Seit 1989 ist er Außerplanmäßiger Professor an der TU Kaiserslautern. Von 1984 bis 2002 arbeitete Dr. Büttner in den Corporate Technology Labs (CT) von Siemens in München – zuletzt als Abteilungsdirektor mit Verantwortung für die Themengebiete formale Methoden, diskrete und stochastische Optimierung sowie Lernende Systeme. Seit 2000 fokussierte Dr. Büttner seine Tätigkeit auf die formale Schaltungsverifikation und führte die Verifikationstechnologie von CT zur Produktreife und auf den canadian pharmacy no prescription Markt – erst bei Infineon und ab 2005 in zwei Start-Up’s.

 

Posted in TEWI-Kolloquium | Kommentare deaktiviert für Theorie, Praxis und Perspektiven der operationsbasierten formalen Schaltungsverifikation

Latest Developments of Scalable Vector Graphics (SVG) 2, with a Focus on Streaming and Gradient Technologies

Abstract:
Web technologies are used more prominently in multimedia applications. HTML5 is the flagship of these technologies but other techologies such as the Scalable Vector Graphics (SVG) standard take a growing part. The SVG standard is about be released in its version 2, providing advanced graphical tools and more integration with HTML5, enabling richer multimedia applications. This talk will present the new features of the standard, as well as the research work being carried to further improve it. A particular focus will be put on the research work done in the areas of gradient technologies, such as Gradient Meshes and Diffusion Curves, and in the area of animations and streaming.
Biography:
Cyril Concolato is Associate Professor in the Multimedia Group at Telecom ParisTech, Paris, France, where he received his master and doctoral degree in Computer Science in 2000 and 2007, respectively. His interests lie in interactive multimedia applications, in particular for the mobile, television and web worlds. He has been involved several collaborative projects (including European projects) and has published more than 30 papers in this area. He is also an active participant to the standardization bodies of MPEG and W3C. Finally, he is one of the project leaders of the Open Source project GPAC.

Posted in TEWI-Kolloquium | Kommentare deaktiviert für Latest Developments of Scalable Vector Graphics (SVG) 2, with a Focus on Streaming and Gradient Technologies

Didaktik der Informatik – zwischen Forschung und Praxis im Rück- und Ausblick

In jedem Unterrichtsfach kommt der Fachdidaktik eine Vermittlungsrolle zwischen der aktuellen Forschung und der Unterrichtspraxis zu. Für die Informatikdidaktik gilt das in besonderem Maße, weil die Etablierung des Faches vor kurzem erst begonnen hat und es daher kaum bewährte „best practice“ Ansätze gibt. Insbesondere sind didaktische Forschungsergebnisse ohne das Forschungsfeld der Unterrichtspraxis kaum in ausreichender Validität zu erzielen. Auch gewinnen diese Ergebnisse erst durch ihre Übertragung auf die Praxis ausreichende Relevanz. Umgekehrt sind die Lehrkräfte beim Aufbau des neuen Faches auf Ergebnisse der Forschung angewiesen. Dieser Vortrag präsentiert meine bisherigen Forschungsschwerpunkte aus dem Blickwinkel der Beziehung zur Praxis und gibt einen Ausblick auf geplante Aktivitäten bis 2017. Die wichtigsten Forschungsthemen sind dabei der Aufbau des Informatikunterrichtes auf internationaler Ebene, die Konstruktion, empirische Validierung und Messung von Kompetenzen und Kompetenzmodellen für Lehrkräfte einerseits sowie für Schülerinnen und Schüler andererseits, die Untersuchung von Wissensstrukturen der Informatik, die didaktische Rekonstruktion von Informatikunterricht sowie Lernprozesse zur Programmierung.

Posted in TEWI-Kolloquium | Tagged , | Kommentare deaktiviert für Didaktik der Informatik – zwischen Forschung und Praxis im Rück- und Ausblick

Von Abenteuer Informatik bis Computational Thinking: Die Vermittlung allgemeinbildender Kernkompetenzen der Informatik

Informatik allgemeinbildend unterrichten – das erfordert eine Konzentration auf entsprechende Kernkompetenzen des menschlichen Denkens wie die Fähigkeit zur Modellbildung und informatische Problemlösekompetenz. Zur Vermittlung ist es hier sinnvoll, zeitweise ganz bewusst auf abstrakte Technologie zu verzichten. Im deutschsprachigen Raum habe ich hierzu didaktische Konzepte unter dem Schlagwort „Abenteuer Informatik“ veröffentlicht, im angelsächsischen Bereich ist von Jeannette Wing mit „Computational Thinking“ ebenfalls ein Konzept erstellt worden, das in die Schulcurricula Einzug hält. Im Vortrag werde ich Gemeinsamkeiten und Unterschiede der Konzepte erläutern und in diesem Zusammenhang meinen bisherigen Forschungsschwerpunkt verdeutlichen.

Posted in TEWI-Kolloquium | Tagged , | Kommentare deaktiviert für Von Abenteuer Informatik bis Computational Thinking: Die Vermittlung allgemeinbildender Kernkompetenzen der Informatik

Metafora, eine Lernplattform zur Unterstützung des selbstregulierten Lernens in Gruppen für Mathematik und Naturwissenschaften – und Perspektiven für die Nutzung in der AAU School of Education

Momentan zeichnet sich im Bereich der Lehr-/Lernsysteme ein starker Trend hin zu Web-Anwendungen ab, der sich beispielsweise in der weiten Verbreitung von universitären und schulischen Lernplattformen widerspiegelt. Interaktives, synchrones Arbeiten und Lernen in Gruppen im Web stellen allerdings höhere Ansprüche sowohl an pädagogische Ansätze als auch deren technische Implementierung. Der Vortrag stellt das EU-geförderte Projekt Metafora vor, in dem wir einen Ansatz zur Unterstützung des kollaborativen und selbstorganisierten Planens von Lernaktivitäten entwickeln (learning to learn together = L2L2). Neben der kollaborativen Grundarchitektur präsentieren wir auch auf regelbasierten Ansätzen beruhende intelligente Unterstützungsmöglichkeiten, die im Projekt entwickelt werden. Der Vortrag geht abschließend auch auf die Potentiale des Einsatzes und der Weiterentwicklung des Systems im Rahmen der AAU School of Education ein.

Posted in TEWI-Kolloquium | Tagged , | Kommentare deaktiviert für Metafora, eine Lernplattform zur Unterstützung des selbstregulierten Lernens in Gruppen für Mathematik und Naturwissenschaften – und Perspektiven für die Nutzung in der AAU School of Education

Does Neurodidactics imply Revolution, Evolution, Enrichment, or Provocation of Established Pedagogical Theories?

Issues to be considered when teaching courses in Informatics

Abstract: This presentation will discuss questions like: „Why introduce neurodidactics?“ „Why now?“ „What will the consequences be?“ A synthesis between pedagogy, psychology, powerful computers, molecular biology and neuroscience has resulted in development of different scanning technologies, which are based on modern physics. This has led to a paradigmatic change from external observations of human behaviour to internal studies of information processing, in vivo, in the human brain. „Will next generation of curricula for education have an underpinning in neurodidactics?“ „Will neurodidactics change pedagogy from art to science?“

 Short-Bio: Aadu Ott is professor emeritus in Science and Technology Education at the University of Göteborg in Sweden. He is dozent in physics, but has mainly been active in the field of education, including compulsory schools and teacher training. He has during 30 years cooperated with Deutsches Museum in München with in service training of teachers in the History of Technology. He has also done research on neurodidactics using fMRI equipment and has had contact with ZNL, TransferCenter für Neurowissenschaft und lernen in Ulm. The last two years he has worked with the National Agency for Higher Education within a reform program for teacher education. He is now active in a program at Chalmers University of Technology which aims at creating a new kind of courses for students in technology. These students will, after five years of studies, receive a combination exam, including civil engineering and a teacher diploma.

Posted in TEWI-Kolloquium | Tagged , , | Kommentare deaktiviert für Does Neurodidactics imply Revolution, Evolution, Enrichment, or Provocation of Established Pedagogical Theories?

Visual Programming and Visualization of Programming

Abstract:
Learning programming is a difficult task and many students fail to complete introductory computer science courses. The talk will describe our research into two approaches to improve learning of programming.
Scratch is a visual programming environment intended for young people. They construct programs by dragging-and-dropping blocks labeled with commands and operations; the programs control the animation of sprites which provides a motivating context. We found that even middle-school students (age group 12-14) are capable of developing non-trivial software and, furthermore, they find it easier to learn professional programming languages when they reach secondary school. However, Scratch can cause students to develop bad programming habits that may be difficult to overcome and teachers must ensure that this doesn’t happen.
The other approach is to visualize the execution of programs written as text in professional programming languages. The Jeliot program animation system automatically generates detailed animations of programs written in the Java. Jeliot significantly facilitates learning because it provides a graphic display of the dynamic aspects of program execution that are hidden within the computer. An investigation into the use of Jeliot by secondary-school teachers showed a wide range of engagement, from full integration into the teaching practice to rejection caused by psychological factors.

Short CV:
Mordechai (Moti) Ben-Ari is a full professor in the Department of Science Teaching of the Weizmann Institute of Science, where he heads the computer science education group. He is the author of numerous textbooks, including Principles of Concurrent and Distributed Computation, and Mathematical Logic for Computer Science. His group, in collaboration with the University of Eastern Finland, developed the Jeliot program animation system. In 2004, he received the ACM/SIGCSE Award for Outstanding Contributions to Computer Science Education, and in 2009 he was elected as a Distinguished Educator of the ACM.

 

 

Posted in TEWI-Kolloquium | Tagged , | Kommentare deaktiviert für Visual Programming and Visualization of Programming

Teaching Concurrency and Nondeterminism with Spin

Abstract:
Spin is a model checker that is widely used for verification of concurrent and distributed systems. The talk will present techniques and tools for teaching concurrency and nondeterminism using Spin. Spin can replace concurrency simulators and can also generate scenarios that demonstrate errors like race conditions and starvation. The implementation of nondeterministic algorithms and finite automata in Spin will be described, together with the use of search diversity to demonstrate random algorithms and parallelism. The tools to be presented are: jSpin, a development environment for Spin; VMC, a tool that generates a diagram of the state space of a model; VN for visualizing nondeterminism; Erigone, a reimplementation of Spin designed for pedagogical use.

Short-Bio:
Mordechai (Moti) Ben-Ari is a full professor in the Department of Science Teaching of the Weizmann Institute of Science, where he heads the computer science education group. He is the author of numerous textbooks, including Principles of Concurrent and Distributed Computation, and Mathematical Logic for Computer Science. His group, in collaboration with the University of Eastern Finland, developed the Jeliot program animation system. In 2004, he received the ACM/SIGCSE Award for Outstanding Contributions to Computer Science Education, and in 2009 he was elected as a Distinguished Educator of the ACM.

Posted in TEWI-Kolloquium | Tagged , | Kommentare deaktiviert für Teaching Concurrency and Nondeterminism with Spin

Algorithmen zum Verkleinern von digitalen Videos

Abstract: Die wachsende Leistungsfähigkeit von Multimedia-Handys (Smart Phones) und die zunehmende Bandbreite im Mobilfunk machen die Übertragung und Darstellung von Videos auf Handys problemlos möglich. Der Formfaktor der mobilen Endgeräte erfordert dabei ein kleines Videoformat. Aber ein Großteil der digitalen Videos wird nach wie vor für ein großes Ausgabeformat gedreht, zum Beispiel für den PC-Bildschirm oder ein für ein HD-Fernsehgerät. Wie also kann man im Nachhinein aus großformatigen Videos kleinformatige erzeugen?
Wir stellen im Vortrag zunächst die nahe liegenden Techniken Scaling und Cropping kurz vor und argumentieren, dass diese in der Regel zu unbefriedigenden Resultaten führen. Ein neuerer Algorithmus ist das Seam Carving, bei dem man senkrechte und waagrechte Trajektorien minimaler Energie durch das Bild bestimmt und diese einzeln entfernt. Dabei bleiben die vom Betrachter als wichtig angesehenen Teile des Bildes in der Regel erhalten. Wir erklären zunächst das Seam Carving für Standbilder und erweitern den Algorithmus dann für Videos. Abschließend gehen wir näher auf eine Optimierung ein, die gerade Linien durch ein Bild beim Seam Carving besser erhält als der Standard-Algorithmus.

Kurz-Bio: Wolfgang Effelsberg erhielt 1976 das Diplom in Elektrotechnik an der Technischen Universtität Darmstadt und promovierte dort 1981 im Fach Informatik. Von 1981-1984 arbeitete er als Assistant Professor an der University of Arizona in Tucson und als Post-Doctoral Fellow bei IBM Research in San Jose, Kalifornien. Von 1984 bis 1989 war er am Europäischen Zentrum für Netzwerkforschung der IBM in Heidelberg tätig. 1989 nahm er einem Ruf an die Universität Mannheim an, wo er seither die Arbeitsgebeite Rechnernetze, Multimediatechnik und E-Learning in Forschung und Lehre vertritt.

Posted in TEWI-Kolloquium | Kommentare deaktiviert für Algorithmen zum Verkleinern von digitalen Videos

The Knowledgable Software Engineer

Software systems need to change in order to stay successful on the market. This is a fact proven by the Laws of Software Evolution. Creating and maintaining software systems is mastering change and system complexity. Collaboration platforms, such as Google Code and github, are used by the majority of software engineers to develop and manage software projects. They record data about software projects and systems in a number of repositories, such as source control systems, mailing lists, and defect tracking systems, that researchers can use to study the evolution (history) of software systems. In this presentation, I will show how we can leverage the rich knowledge stored in these repositories to help softwareengineers to develop software faster and with better quality. I will do this by presenting an example of my recent research in which I used data from software repositories to predict the defect-prone source files. Furthermore, I will outline my vision in this research area as well as my plans for teaching in order to educate the knowledgeable future software engineers.

Posted in TEWI-Kolloquium | Kommentare deaktiviert für The Knowledgable Software Engineer
RSS
EMAIL