E.D. Schabell, and S.J.B.A. (Stijn) Hoppenbrouwers. Empowering Full Scale Straight Through Processing with BPM. Technical report: ICIS-R08004, February, SNS Bank, 2009.
The SNS Bank (the Netherlands) has made a strategic decision to empower her customers on-line by fully automating her business processes. The ability to automate these service channels is achieved by applying Business Process Management (BPM) techniques to existing selling channels. Both the publicly available and internal processes are being revamped into full scale Straight Through Processing (STP) services. This extreme use of on-line STP is the trigger in a shift that is of crucial importance to cost effective banking in an ever turbulent and changing financial world. The key elements used in implementing these goals continue to be (Free) Open Source Software (FOSS), Service oriented architecture (SOA), and BPM. In this paper we present an industrial application describing the efforts of SNS Bank to make the change from traditional banking services to a full scale STP and BPM driven bank.
Jozef Hooman, and Marcel Verhoef. Formal Semantics of a VDM Extension for Distributed Embedded Systems. Technical report: ICIS-R09005, December, Radboud University Nijmegen, 2009.
To support model-based development and analysis of embedded systems, the specification language VDM++ has been extended with asynchronous communication and improved timing primitives. In addition, we have defined an interface for the co-simulation of a VDM++ model with a continuous-time model of its environment. This enables multi-disciplinary design space exploration and continuous validation of design decisions throughout the development process. We present an operational semantics which formalizes the precise meaning of the VDM extensions and the co-simulation concept.
Sander D. Vermolen, Jozef Hooman, and Peter Gorm Larsen. Proving Consistency of VDM models using HOL. Technical report: ICIS-R09006, December, Radboud University Nijmegen, 2009.
Although consistency of formal models is crucial, consistency proofs should not be a large burden to the user. Hence, it is important to have access to efficient proof support which is able to automate a large part of the consistency proofs. We have developed a tool that automatically translates a large subset of VDM and its associated proof obligations, which ensure model consistency, to the theorem prover HOL. In addition, powerful tactics have been constructed to discard most of the proof obligations automatically. The application of our approach to four case studies shows that a high degree of automation can be achieved.