This post originated from an RSS feed registered with Java Buzz
by Paul Brown.
Original Post: BPEL für WS, Petri Nets, and Formalism
Feed Title: mult.ifario.us
Feed URL: http://feeds.feedburner.com/MultifariousCategoryJava
Feed Description: Software. Business. Java. XML. Web Services.
I wanted to get the classic traffic light example working in a Petri net simulator for a talk I gave last week on BPM, workflow, Petri nets, and pi-calculus, but I ran out of time. (I'll post the slides later.)Fortunately (and, appropriately after the talk), I came across the Petri Net Kernel ("PNK") project from the Institut für Informatik at Humboldt-Universität zu Berlin, which provides a useful framework and tools for working with Petri nets in Java.It turns out that a group at the Institut has a "Task Force BPEL4WS" that has been working on items related to BPEL. The site has a mixture of publications that vary from seminar slides to student projects to some dissertations and papers. If you can read technical German (or can limp along with Sherlock or the equivalent), Axel Martens's dissertation Verteilte Geschäftsprozesse - Modellierung und Verifikation mit Hilfe von Web Services is worth a look. Axel's work also includes some software built on the PNK (and that requires a few trivial tweaks to run on non-Windows OSs) to perform static analysis of BPEL processes via Petri net representations.(For an approach based on process algebras, see a paper by Franck van Breugel and Mariya Koshkina that uses the Concurrency Workbench to perform analysis.)It's good to see people working on constructive approaches to formal static analysis of BPEL processes. Unit testing, integration testing, code coverage, etc., can only provide a level of confidence that a system will not fail in expected ways, but formal analysis can prove that a system will not fail at all. I've seen enough obscure, expensive, and unexpected software failures to believe that this has to be one of the things that we collectively value when selecting new tools and technologies.