Florian Leitner-Fischer

A collection of books discussing functional safety according to ISO61508 and ISO26262.

English:

Functional Safety
The Safety Critical Systems Handbook

German:

Funktionale Sicherheit
Funktionale Sicherheit in der Praxis

It’s december and a new year will start a few days from now. It’s that time of the year where we think of thinks we want to achieve or do more often the next year. Often theses things include sports, losing weight or spending more time with loved ones.
These are all valid and important new years resolutions and you should go for them. But there is one more thing, let’s think about how we can sharpen our saws to become better at our work. This list is primarily intended for computer scientists and software engineers, developers and architects but probably can be adapted for other professions as well.

Here’s some ideas, some mine, some are inspired by a similar post of Scott Hanselman:

• Set-aside time, like one or two hours per week, to read technical books or papers related to your field of work.
• Set-aside time to read one technical paper or book that is not related to your field of work per month.
• Listen to podcasts, or watch screencasts about new technologies and approaches.
• Attend conferences and talks and most importantly try to ask questions or at least write down questions and try to figure out the answer for your self.
• Discuss problems with your co-workers, you might be surprised how much you can learn from a good discussion.
• Help others, sometimes there is no better and satisfactory way than helping someone to solve a technical problem.
• Try something new! Whether it is a new programmin language, new software architecting tool or a new software process model you’ll never know when you need it.

The last few months I had not much time to blog, but today I want to write about a current research project
I’m involved in.

The QuantUM Approach

When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Also, it is necessary that the description methods used do not require a profound knowledge of formal methods. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. All inputs of the analysis are specified at the level of a UML model. This model is then automatically translated into the analysis model, and the results of the analysis are consequently represented on the level of the UML model. Thus the analysis model and the formal methods used during the analysis are hidden from the user.

Our approach depicted in the Figure above can be summarized by identifying the following steps:

• Our UML extension is used to annotate the UML model with all information that is needed to perform a dependability analysis.
• The annotated UML model is then exported in the XML Metadata Interchange (XMI) format which is the standard format for exchanging UML models.
• Subsequently, our QuantUM Tool parses the generated XMI file and generates the analysis model in the input language of the probabilistic model checker PRISM as well the properties to be verified.
• For the analysis we use the probabilistic model checker PRISM together with DiPro in order to compute probabilistic counterexamples representing paths leading to a hazard state.
• The resulting counterexamples can then be transformed into a fault tree that can be interpreted at the level of the UML model. Alternatively, they can be mapped onto a UML sequence diagram which can be displayed in the UML modeling tool containing the original UML model.

Key Features of QuantUM

QuantUM Profile for UML and SysML

Extension of the UML and SysML with stereotypes. Specification of safety requirements, dependability characteristics (failure modes, …), failure propagation, component dependencies, safety mechanisms (repair management, redundancy structures) directly in the architectural model with your existing UML / SysML CASE tool.

Probabilistic Analsysis / pFMEA

The annotated UML Model is automatically translated into the input language of a probabilistic model checker, which computes the probability of  safety requirements of hazards. In addition a probabilistic FMEA can be performed automatically.

Automated Fault Tree Generation

(Quantitative) Fault Trees identifying the events causing the violation of a safety requirement or a hazard are automatically generated the analysis.

Result Representation in UML / SysML

System executions violating safety requirements or causing a hazard can be displayed as UML sequence diagrams.

Industrial Usage

The QuantUM approach was applied in several industrial case studies and can be used with all major UML / SysML case tools (e.g. IBM Rational Rhapsody, IBM Rational Software Architect, Sparxsystem Enterprise Architect, …)

More Information

More Information on the theory and methods behind QuantUM can be found on the publications site. As soon as the first prototype is available
it will be announced here! Stay tuned!

After many months of implementation and testing we finally released the DiPro tool for probabilistic counterexample generation tool.
I will give a talk on DiPro’s features on the SPIN 2011 Workshop (July 14-15), co-located with CAV 2011 in Snowbird Utah.

What is DiPro?

Current stochastic model checkers do not make counterexamples for property violations readily available. DiPro is a tool, that applies directed explicit state space search to discrete- and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties.

Directed explicit state space search algorithms explore the state space on-the-fly which makes DiPro very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method.

Counterexamples provided by DiPro have two important properties. First, they include those traces which contribute the most amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes.

DiPro allows for the computation of counterexamples for the stochastic model checkers PRISM or MRMC.

Download DiPro here.

Hier habe ich bereits über den Hama WLAN Stick für Samsung Fernseher als Alternative für den original Samsung WLAN Stick geschrieben.

Noch mal alle Infos in kürze:

Den Samsung original Stick gibt es bei Amazon schon für um die 70 Euro.

Wem das zu teuer ist kann sich auch den Hama MiMO Wlan USB2.0 Adapter für unter 30 Euro kaufen.

Mit folgenden Samsung Geräten wurde der Hama MiMO Wlan USB2.0 Adapter als alternative zum Samsung Stick getestet:

Mein Tipp: Den Hama MiMO Wlan USB2.0 Adapter bei Amazon.de kaufen, dann könnt Ihr ihn testen und wenn er an Eurem Samsung Gerät doch nicht funktionieren sollte, könnt Ihr ihn problemlos innerhalb von 2 Wochen an Samsung zurücksenden.

Die  Installationsanleitung für den Hama WLAN Stick am Samsung TV findet ihr hier, und hier die Liste mit kompatiblen Samsung TVs und Blu-Ray Player.

Seit kurzem gibt es nun von Hama eine 3D Brille, die mit den Samsung TVs kompatible ist.

Mit einem Preis von rund 80 Euro, liegt die Brille zwischen der Samsung SSG-2100 und der Samsung SSG-2200.

Ich werde die Brille in kürze testen und hier darüber berichten.

16.12.2010 Kurzes Update:

Twonky kann man mittlerweile in der Version 6.0.30 auch für die MyBookWorld Festplatte herunterladen, damit funktioniert nun auch MKV Streaming problemlos.
Installationsanleitung folgt.

Ein sehr schönes Feature der neuen Samsung TVs ist, dass sie alle möglichen Audio-, Video- und Bild-Dateien streamen können. Hierzu muss man den Fernseher per WLAN oder Kabel mit dem Netzwerk verbinden. Danach werden in MediaPlay alle im lokalen Netzwerk verfügbaren Server angezeigt.

Befindet sich beispielsweise ein Windows 7 Rechner im Netz, werden alle Dateien der Windows Media Player Mediathek angezeigt. Außerdem kann man mit dem PC Share Manager von Samsung auch Ordner freigeben.  Wenn man jedoch nach Samsung TV und MKV oder Samsung TV Streaming googled, sieht man schnell das die oben genannten Streaming Server leider nicht alle vom Samsung TV unterstützen Formate unterstützen.

Nach dem ich nun ein paar verschiedene Streaming Server getestete habe, komme ich zu dem Schluss das nur der Twonky Media Server in der neusten Version (6.0.28) alle Dateien (einschließlich mkv) richtig zum Samsung Fernseher streamed. Und mit 14,95 Euro für eine Lizenz ist er eine super Anschaffung. Die Version 6-0-28 gibt es im Moment für Windows, Linux und Mac OSX.

Ich warte nun sehnsüchtig auf die Version für NAS Festplatten, welche ich dann auf meiner Western Digital MyBookWorld Platte installieren werde. Sobald ich die neue Twonky Version auf der MyBookWorld installiert habe, gibt es hier natürlich einen ausführlichen Bericht + Anleitung.

My master’s thesis is now available online here.

Abstract

When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Another obstacle is, that the methods often require a profound knowledge of formal methods, which can rarely be found in industrial practice. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.

Wie bereits erwähnt, ist der Hama MiMO Wlan USB2.0 Adapter für unter 30 Euro eine günstige Alternative zum Samsung original USB WLAN Dongle um die seinen neuen Samsung TV oder Blu-Ray Player mit dem Internet zu verbinden. Die Liste mit den kompatiblen Samsung Geräten gibt es hier.

Hier habe ich nun eine Installationsanleitung inkl. Screenshots erstellt:

• Schließen Sie den WLAN-Adapter an das Fernsehgerät an.
  Wenn der WLAN-Adapter eingerichtet ist, wird ein Popup-Fenster geöffnet.

• Wählen Sie “Allg. Einstell.”.

• Wählen Sie im Fenster Netzwerk “Netzwerktyp” und stellen Sie Netzwerktyp auf “Drahtlos”.
• Wählen Sie Eingang einrichten. Das Fenster Eingang einrichten wird geöffnet.

• Wählen Sie “Wählen Sie ein Netzwerk” durch Drücken der Taste ▲, und drücken Sie dann die ENTER-Taste. Die Netzwerkfunktion sucht nach verfügbaren Funknetzwerken. Nach Abschluss der Suche wird eine Liste der verfügbaren Netzwerke angezeigt.

• Markieren Sie durch Drücken der Tasten ▲ oder ▼ ein Netzwerk in der Netzwerkliste, und drücken Sie dann die ENTER-Taste. Wenn der Zugangspunkt ausgeblendet (versteckt) ist, müssen Sie Netzwerk hinzufügen wählen und den Name des Netzwerks (SSID) sowie den Sicherheitsschlüssel richtig eingeben, um die Verbindung aufzubauen.

• Geben Sie im Fenster Sicherheit das Kennwort Ihres Netzwerks ein.
  Bei der Eingabe des Kennworts beachten Sie diese allgemeinen Hinweise:
  • Drücken Sie auf die Zifferntasten Ihrer Fernbedienung, um Zahlen einzugeben.
  • Verwenden Sie die Navigationstasten Ihrer auf der Fernbedienung, um im Fenster Sicherheitsschlüssel zwischen den Schaltflächen zu wechseln.
  • Drücken Sie die rote Taste, um zwischen Groß- und Kleinschreibung umzuschalten oder um Zeichen/ Symbole anzuzeigen.
  • Wenn Sie einen Buchstaben oder ein Symbol eingeben möchten, navigieren Sie zu dem Buchstaben oder Symbol und drücken Sie dann die ENTER-Taste.
  • Um den letzten Buchstaben oder die letzte Zahl zu löschen, drücken Sie auf die grüne Taste Ihrer Fernbedienung.
• Wenn Sie fertig sind, drücken Sie die blaue Taste Ihrer Fernbedienung. Das Fenster Netzwerkverbindung wird geöffnet. Warten Sie, bis die Verbindungsbestätigung angezeigt wird, und drücken Sie dann die ENTER-Taste. Das Fenster Eingang einrichten wird wieder angezeigt.

• Um die Verbindung zu testen, drücken Sie die Taste RETURN, um Netzwerktest zu wählen, und drücken Sie dann die ENTER-Taste.

Der e-Tailer Amazon.de hat viele Blu-Ray Player im Preis gesenkt, darunter auch der Samsung BD-C6900 3D-Blu-Ray Player und der Samsung BD-C5500. Erfahrungsgemäß steigen die Preise zum Jahresende wieder an. Also schnell zuschlagen!