DiPro – Directed Probabilistic Counterexample Generation Tool Released

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.

Streaming Server für Samsung TVs

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.


Mac OSX Text Editor: TextWrangler

On my Windows computers I use Notepad++ for editing text files like html, css, php and other script files. Now, that I’m using a MacBook Pro as work computer, I searched for an equivalent text editor.

The features I need are:

  • Freeware
  • Syntax Highlighting
  • Comparing Files
  • Good Search / Replace capabilities

After I tested a few editors, I stuck with TextWrangler which also offers nice features like editing files on a SSH / FTP server.

Tool List

Yesterday I received my new quad core PC and I want to present a list of software tools that I don’t want to miss:

%41%43%45%20%54%65%61%6d

Was soll uns %41%43%45%20%54%65%61%6d wohl sagen?

“Übersetzt” bedeutet es ACE Team oder genauer (Microsoft) Application Consulting & Engineering Team. Was kann man sich darunter vorstellen? Dieses Team besteht hauptsächlich aus IT-Security Spezialisten (= Hackern) die Sicherheitslücken aufdecken und helfen diese zu vermeiden.

Der jüngste Post widmet sich Sicherheitslücken in Web-Applikationen.

First Line of Defense for Web Applications – Part 1

Google Browser Sync

Wer häufig an mehreren Rechnern arbeiten kennt das folgende Problem sicher: Man weiß das man einen Link in seinen Favoriten hat und braucht diesen genau jetzt, sitzt aber am falschen Rechner. Hier mit ist jetzt Schluss! Mit der Firefox Erweiterung Google Browser Sync kann man seine Favoriten auf allen Rechnern synchronisieren und als kleiner Bonus hat man auch immer noch ein Backup von diesen. Wenn man möchte, kann man mit dieser Erweiterung sogar ganze Firefox Sessions, die History und gespeicherte Passwörter synchronisieren. 

Papier ist böse!

  “Papier ist böse und gefährlich den es hat scharfe Kannten“ um Rodney an dieser Stelle mal zu zitieren.

Bei Coding 4 Fun habe ich nun ein interessantes Projekt gefunden, welches endlich im Kampf gegen das böse Papier helfen kann ;).
Mittels Scanner lassen sich Dokumente erfassen, welche man dann zusammen mit Meta-Daten speichern kann. Man kann (muss) zwar noch ein paar Sachen an dem Tool Verbessern um es zu einer richtigen Dokumenten Verwaltung zu machen aber auf jeden Fall ist der erste Schritt getan.

Vista Battery Saver

Mit der Installation von Windows Vista vor über 8 Monaten, wurde die “Lebensdauer” meines Notebooks Akkus in etwa halbiert.

das lag vor allem daran, dass ich auch im Akku betrieb, Aero aktiviert hatte, weil ich nicht immer wenn ich das Notebook vom Netz genommen habe umschalten wollte.

Eine Lösung für dieses Problem ist der Vista Battery Saver, der Aero automatisch beim Wechsel in den Akku Betrieb ausschaltet und beim einstecken des Netzkabels wieder anschaltet.

Windows Live Writer 1.0 hat Probleme mit Umlauten

Bei meinem letzten Post ist mir aufgefallen, das der Windows Live Writer Version 1.0 Beta Deutsch, noch Probleme mit deutschen Umlauten hat.

Dies liegt daran, das der Live Writer die Umlaute nicht HTML-Escape Tags umbaut. Sprich ein ä bleibt auch im HTML Code ein ä und wird nicht zu ä. Deswegen wird der Post dann nach dem ersten ä, ö oder ü abgeschnitten.

Beheben lässt sich dies im Moment nur durch ein umschalten in die HTML-Ansicht und ein händisches ersetzen von ä durch ä, ö durch ö und ü durch ü.