[1] Máté Kovács, Dániel Varró, and László Gönczy. Formal Analysis of BPEL Workflows with Compensation by Model Checking. International Journal of Computer Systems Science and Engineering, 2008. To Appear.
[ bib ]
In the paper, we present an approach for the verification of business workflows – captured by BPEL processes – with full support for compensation and fault handling. BPEL processes are transformed into the SAL language to carry out (i) verification of safety and reachability properties and (ii) fault modeling by using the SAL symbolic model checker. Compared to existing solutions for model checking BPEL processes, the main added value of the paper is that (i) potential error propagation paths can also be assessed in addition to traditional verification tasks, and (ii) our approach scales up to relatively large workflows thanks to abstraction techniques and the use of the advanced SAL model checker.
[2] Gyula Simon, Miklós Molnár, László Gönczy, and Bernard Cousin. Robust k-coverage Algorithms for Sensor Networks. IEEE Transactions on Instrumentation and Measurement, 57, August 2008. To Appear.
[ bib ]
[3] László Gönczy, István Majzik, Akos Horváth, Dániel Varró, András Balogh, Zoltán Micskei, and András Pataricza. Tool Support for Engineering Certifiable Software. In Michaela Huhn and Hardi Hungar, editors, Proc. of First Workshop on the Certification of Safety-Critical Software Controlled Systems (SafeCert08), pages 68-73, Budapest, Hungary, 2008.
[ bib ]
Formal methods can effectively support the model driven develoment and analysis of IT applications in many domains. Typically, the domain-specific engineering models are transformed to formal analysis models (to compute measures that help the designer in verifying the design decisions) and verified models are mapped to test and implementation related software artefacts. An overview of four European projects demonstrates the use of support tools and tool integration facilities in development processes of systems having in sight the demand of certification according to domain-specific standards.
[4] Máté Kovács, Dániel Varró, and László Gönczy. Formal Modeling of BPEL Workflows Including Fault and Compensation Handling. In Proc. of Engineering Fault Tolerant Systems (EFTS2007), Dubrovnik, Croatia, 2007.
[ bib ]
Electronically executed business processes are frequently implemented using the Business Process Execution Language (BPEL). These workflows may be in control of crucial business processes of an organization, in the same time existing model checking approaches are still immature i.e. they either seem to loose to much information during the generation of the analysis model, or the state space explosion prevents from model checking. We present a formal modeling technique for BPEL workflows including fault and compensation handling providing exact semantics with a state space size that allows for model checking. Additionally, error propagation among variables is supported so the effect of a faulty activity on the entire process can be examined.
[5] László Gönczy, Reiko Heckel, and Dániel Varró. Model-based Testing of Service Infrastructure Components. In Petrenko et al., editor, Proc. of TESTCOM/FATES 2007, volume 4581 of Lecture Notes in Computer Science, Tallinn, Estiona, 2007. Springer.
[ bib ]
We present a methodology for testing service infrastructure components described in a high-level (UML-like) language. The technique of graph transformation is used to precisely capture the dynamic aspect of the protocols which is the basis of state space generation. Then we use model checking techniques to find adequate test sequences for a given requirement. To illustrate our approach, we present the case study of a fault tolerant service broker which implements a well-known dependability pattern at the level of services. Finally, a compact Petri Net representation is derived by workflow mining techniques to generate faithful test cases in a non-deterministic, distributed environment. Note that our methodology is applicable at the architectural level rather than for testing individual service instances only.
[6] László Gönczy. Methodology for a Precise Development Process of Service Oriented Applications. In Young Researchers Conference on Service Oriented Computing (YR-SOC2007), Leicester, UK, 2007.
[ bib ]
[7] Gyula Simon, Miklos Molnár, László Gönczy, and Bernard Cousin. Dependable k-coverage Algorithms for Sensor Networks. In Instrumentation and Measurement Technology Conference (IMCT2007), May 1-3, 2007, Warsaw, Poland, 2007.
[ bib ]
[8] László Gönczy, János Ávéd, and Dániel Varró. Model-based Deployment of Web Services to Standards-compliant Middleware. In Immaculada J. Martinez Pedro Isaias, Miguel Baptista Nunes, editor, Proc. of the Iadis International Conference on WWW/Internet 2006(ICWI2006). Iadis Press, 2006.
[ bib ]
Nowadays, due to the rapid increase in the number of available web services, more and more emphasis is put on their reliability, availability, security, etc. In order to meet such non-functional requirements, a service needs to be designed for reliability by making design decisions on a high, architectural level. Fortunately, web service related standards also include how to provide reliable messaging between services (e.g. in WS-ReliableMessaging and WS-Reliability). Several frameworks (like RAMP, RM4GS) implement the standard to provide a reliability middleware. However, these standards typically offer very low, XML-level mechanisms for specifying the reliability parameters of web services when deploying them to a reliability middleware. For this purpose, we propose a model-driven approach for the deployment of web services to standards-compliant reliable middleware. The actual XML descriptors are generated automatically from platform-independent description of services enriched with reliability attributes by model transformations.
[9] László Gönczy, Máté Kovács, and Dániel Varró. Modeling and Verification of Reliable Messaging by Graph Transformation Systems. In Proc. of the Workshop on Graph Transformation for Verification and Concurrency (GTVC2006). Elsevier, 2006.
[ bib | .pdf ]
Due to the increasing need of highly dependable services in Service-Oriented Architectures (SOA), service-level agreements include more and more frequently such non-functional aspects as security, safety, availability, reliability, etc. Whenever a service can no longer be provided with the required QoS, the service requester needs to switch dynamically to a new service having adequate service parameters after exchanging a sequence of messages. In the current paper, we first extend the core SOA metamodel with parameters required for reliable messaging in services. Then we model reconfigurations for reliable message delivery by graph transformation rules. Finally, we carry out a formal verification of the proposed rule set by combining analysis tools for graph transformation and labeled transition systems.
[10] András Pataricza, András Balogh, and László Gönczy. Enterprise Modeling and Computing with UML, chapter Verification and Validation of Non-functional Aspects in Enterprise Modeling, pages 261-303. Idea Group, 2006.
[ bib ]
[11] Erwin Schoitsch, Egbert Althammer, Henrik Eriksson, Jonny Vinter, László Gönczy, András Pataricza, and György Csertán. The DECOS Test Bench - Execution of Verification and Validation Activities and Tool Integration. In Proc. of Informationstagung Mikroelektronik ME 2006, October 11-12 2006.
[ bib ]
The integrated EU-project DECOS (Dependable Embedded Components and Systems) aims at develop-ing an integrated architecture for embedded systems to reduce life-cycle costs and to increase depend-ability of embedded applications. To facilitate the certification process of DECOS-based applications, the DECOS Test Bench constitutes a framework to support incremental Validation and Verification as well as modular certification on the basis of generic safety cases. The safety cases are based on validation-plans (v-plans) comprising the steps to validate the safety requirements (called V&V-activities). This paper focuses on two aspects of the Test Bench: the execution of V&V-activities and the integration of V&V-tools into the Test Bench framework.
[12] Erwin Schoitsch, Egbert Althammer, Henrik Eriksson, Jonny Vinter, László Gönczy, András Pataricza, and György Csertán. Validation and Certification of Safety-Critical Embedded Systems - the DECOS Test Bench. In Proceedings of The 25th International Conference on Computer Safety, Security and Reliability (SAFECOMP2006), Lecture Notes in Computer Science, Gdansk, POLAND, September 25-29 2006. Springer.
[ bib | .pdf ]
The integrated EU-project DECOS (Dependable Embedded Components and Systems) aims at developing an integrated architecture for embedded systems to reduce life-cycle costs and to increase dependability of embedded applications. To facilitate the certification process of DECOS-based applications, the DECOS Test Bench constitutes a framework to support Validation and Verification. By implementing a modular approach, an application safety case merely contains the application-specific issues and reuses the safety arguments of the generic safety cases of the DECOS platform. The Test Bench covers the complete life cycle from the platform-independent models to deployment, including model validation and transformations. The safety cases are based on validation-plans (v-plans) comprising the steps to validate the safety requirements. The Test Bench provides a methods/tools repository, guidelines to generate and execute v-plans, and integration of tools and of remotely distributed test beds.
[13] László Gönczy and Daniel Varró. Modeling of Reliable Messaging in Service Oriented Architectures. In Andrea Polini, editor, Proceedings of International Workshop on Web Services Modeling and Testing (WS-MaTe2006), pages 35-49, Palermo, Sicily, ITALY, June 9th 2006.
[ bib | .pdf ]
Due to the increasing need of highly dependable services in Service-Oriented Architectures(SOA), service-level agreements include more and more frequently such traditional aspects as security, safety, availability, reliability, etc. Whenever a service can no longer be provided with the required QoS, the service requester need to switch dynamically to a new service having adequate service parameters. In the current paper, we propose a metamodel to capture such parameters required for reliable messaging in services in a semi-formal way (as an extension to [1]). Furthermore, we incorporate fault-tolerant algorithms into appropriate reconfiguration mechanisms for modeling reliable message delivery by graph transformation rules.
[14] László Gönczy. Verification of Reconfiguration Mechanisms in Service-Oriented Architectures. In in Proceedings of Conference of PhD Students in Computer Science, page 52, Szeged, HUNGARY, 2006.
[ bib | .pdf ]
[15] László Gönczy, Silvano Chiaradonna, Felicita Di Giandomenico, András Pataricza, Andrea Bondavalli, and Tamás Bartha. Dependability Evaluation of Web Service-Based Processes. In Miklós Telek, editor, Proceedings of European Performance Engineering Workshop (EPEW 2006), Lecture Notes on Computer Science, pages 166-180, Budapest, HUNGARY, 2006. Springer.
[ bib | http ]
As Web service-based system integration recently became the mainstream approach to create composite services, the dependability of such systems becomes more and more crucial. Therefore, extensions of the common service composition techniques are urgently needed in order to cover dependability aspects and a core concept for the dependability estimation of the target composite service. Since Web services-based workflows fit into the class of systems composed of multiple phases, this paper attempts to apply methodologies and tools for dependability analysis of Multiple Phased Systems (MPS) to this emerging category of dependability critical systems. The paper shows how this dependability analysis constitutes a very useful support to the service provider in choosing the most appropriate service alternatives to build up its own composite service.
[16] Máté Kovács and László Gönczy. Simulation and Formal Analysis of Workflow Models. In Roberto Bruni and Daniel Varro, editors, Proc. of the Fifth International Workshop on Graph Transformation and Visual Modeling Techniques, Electronic Notes in Theoretical Computer Science, pages 215-224, Vienna, AUSTRIA, 2006. Elsevier.
[ bib | .pdf ]
We present a framework for the simulation and formal analysis of workflow models. We discuss (i) how a workflow model, implemented in the BPEL language, can be transformed into a data ow network model, (ii) how potentially incorrect execution paths can be incorporated, and (iii) how the properties of a workflow can be formally verifed using the SPIN model checker. For the several model transformation steps from workflow to analysis models, we use graph transformations.
[17] László Gönczy. Dependability Analysis and Synthesis of Web Services. In Proc. 13th PhD Mini-Symposium, Budapest, HUNGARY, 2004.
[ bib ]
[18] László Gönczy. Dependability Analysis of Web Service-based Business Processes by Model Transformations. In Proc. of the First European Young Researchers Workshop on Service Oriented Computing (YR-SOC), pages 32-37, Leicester, UK, 2005.
[ bib | .pdf ]
A typical composite Web service is built of basic Web services, both internal and external, over which the integrator does not have a complete control. The service-based integration of enterprise systems raises the need for the analysis of non-functional characteristics of a composite Web service. Such an analysis should cover dependability (for instance, the reliability of the main process, sensitivity analysis on component reliability, etc.) and performability aspects (e.g. determining the optimal process structure for a given level of reliability) as well. The paper discusses how graph transformations can be used to adapt formal methodologies for analyzing SOA models. This way a flexible and extendable analysis framework can be developed for Web service-based business processes.
[19] László Gönczy, András Pataricza, Felicita Di Giandomenico, Silvano Chiaradonna, and Andrea Bondavalli. Dependability Modeling of Web Service Flows. In Supplementary Volume of the Fifth European Conference on Dependable Computing (EDCC-5), pages 77-78, Budapest, HUNGARY, 2005. Fast Abstract.
[ bib ]
[20] László Gönczy. Design of Reliable Web Services. In Proc. 12th PhD Mini-Symposium, pages 36-37, Budapest, HUNGARY, 2005.
[ bib ]
[21] László Gönczy. Building Complex Systems of Web Services. In Volume of Extended Abtsracts of Conference of PhD Students in Computer Science, page 50, Szeged, HUNGARY, 2004.
[ bib ]
[22] László Gönczy. Web service rendszerek - Systems of Web Services. In Fiatal Mûszakiak Tudományos Ülésszaka (FMTU2004), pages 105-108, Cluj Napoca, ROMANIA, 2004. In Hungarian.
[ bib ]
[23] László Gönczy. Katasztrófa-elhárítás munkafolyamtokban - Disaster Recovery in Workflows. Technical report, Budapest University of Technology and Economics, 2004.
[ bib ]
[24] László Gönczy. Design of Robust Web Services. In Proc. 11th PhD Mini-Symposium, pages 42-43, Budapest, HUNGARY, 2004.
[ bib ]

This file has been generated by bibtex2html 1.79