@ARTICLE{Kovacs-Varro-Gonczy, AUTHOR = {M{\'a}t{\'e} Kov{\'a}cs and D{\'a}niel Varr{\'o} and L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Formal Analysis of BPEL Workflows with Compensation by Model Checking}}, JOURNAL = {International Journal of Computer Systems Science and Engineering}, VOLUME = {}, YEAR = {2008}, NUMBER = {}, SERIES = {}, NOTE = {{To Appear}}, MONTH = {}, ABSTRACT = {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.} }
@ARTICLE{simon08robust, AUTHOR = {Simon, Gyula and Moln\'ar, Mikl\'os and G\"onczy, L\'aszl\'o and Cousin, Bernard}, TITLE = {{Robust k-coverage Algorithms for Sensor Networks}}, JOURNAL = {IEEE Transactions on Instrumentation and Measurement}, VOLUME = {57}, YEAR = {2008}, NUMBER = {}, SERIES = {IEEE}, NOTE = {{To Appear}}, MONTH = {August} }
@INPROCEEDINGS{Safecert08, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy and Istv\'an Majzik and A\'kos Horv\'ath and D{\'a}niel Varr{\'o} and Andr\'as Balogh and Zolt\'an Micskei and Andr\'as Pataricza}, TITLE = {{Tool Support for Engineering Certifiable Software}}, BOOKTITLE = {Proc. of First Workshop on the Certification of Safety-Critical Software Controlled Systems (SafeCert08)}, EDITOR = {Michaela Huhn and Hardi Hungar}, SERIES = {}, PUBLISHER = {}, NOTE = {}, PAGES = {68-73}, YEAR = {2008}, ADDRESS = {Budapest, Hungary}, ABSTRACT = {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.} }
@INPROCEEDINGS{Kovacs-Varro-Gonczy-EFTS07, AUTHOR = {M{\'a}t{\'e} Kov{\'a}cs and D{\'a}niel Varr{\'o} and L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Formal Modeling of BPEL Workflows Including Fault and Compensation Handling}}, BOOKTITLE = {{Proc. of Engineering Fault Tolerant Systems (EFTS2007)}}, EDITOR = {}, SERIES = {}, PUBLISHER = {}, NOTE = {}, YEAR = {2007}, ADDRESS = {Dubrovnik, Croatia}, ABSTRACT = {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.} }
@INPROCEEDINGS{Gonczy-Heckel-Varro-TESTCOM07, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy and Reiko Heckel and D{\'a}niel Varr{\'o}}, TITLE = {{Model-based Testing of Service Infrastructure Components}}, BOOKTITLE = {Proc. of TESTCOM/FATES 2007}, EDITOR = {Petrenko et al.}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {4581}, PUBLISHER = {Springer}, NOTE = {}, YEAR = {2007}, ADDRESS = {Tallinn, Estiona}, ABSTRACT = {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.} }
@INPROCEEDINGS{Gonczy-YRSOC07, AUTHOR = {L\'aszl\'o G\"onczy}, TITLE = {{Methodology for a Precise Development Process of Service Oriented Applications}}, BOOKTITLE = {{Young Researchers Conference on Service Oriented Computing (YR-SOC2007)}}, YEAR = {2007}, ADDRESS = {Leicester, UK}, ABTSRACT = {This paper aims at presenting an engineering process which bridges precisely defined service configurations and standard deployment techniques. Service models are described in a well-founded manner using the SRML language, developed in the SENSORIA FP6 project. These models are then basis of i)an ontology-based validation and ii)deployment of services in the emerging industrial service configuration specification SCA. Reasoning systems allow the developer to validate the consistency of model instances. In the SOA context, e.g. architectural compatibility of the model and the specification can be validated and possible infeasibilities of the metamodel can be identified. The design of an Eclipse-based framework is presented in which most of the MDA-conform development tasks are executed in a (semi-)automated way.} }
@INPROCEEDINGS{Simon-Molnar-Gonczy-Cousin-IMTC07, AUTHOR = {Gyula Simon and Miklos Moln\'ar and L\'aszl\'o G\"onczy and Bernard Cousin}, TITLE = {{Dependable k-coverage Algorithms for Sensor Networks}}, BOOKTITLE = {{Instrumentation and Measurement Technology Conference (IMCT2007), May 1-3, 2007}}, YEAR = {2007}, ADDRESS = {Warsaw, Poland}, ABTSRACT = {Redundant sensing capabilities are often required in sensor network applications due to various reasons, e.g. robustness, fault tolerance, or increased accuracy. At the same time high sensor redundancy offers the possibility of increasing network lifetime by scheduling sleep intervals for some sensors and still providing continuous service with help of the remaining active sensors. In this paper centralized and distributed algorithms are proposed to solve the k-coverage sensing problem and maximize network lifetime. When physically possible, the proposed robust Controlled Greedy Sleep Algorithm provides guaranteed service independently of node and communication errors in the network. The performance of the algorithm is illustrated and compared to results of a random solution by simulation examples.} }
@INPROCEEDINGS{Gonczy-Aved-Varro-ICWI06, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy and J{\'a}nos {\'A}v{\'e}d and D{\'a}niel Varr{\'o}}, TITLE = {{Model-based Deployment of Web Services to Standards-compliant Middleware}}, BOOKTITLE = {Proc. of the Iadis International Conference on WWW/Internet 2006(ICWI2006)}, EDITOR = {Pedro Isaias, Miguel Baptista Nunes, Immaculada J. Martinez}, SERIES = {}, PUBLISHER = {Iadis Press}, NOTE = {}, YEAR = {2006}, ABSTRACT = {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.} }
@INPROCEEDINGS{Gonczy-Kovacs-Varro-GTVC06, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy and M{\'a}t{\'e} Kov{\'a}cs and D{\'a}niel Varr{\'o}}, TITLE = {{Modeling and Verification of Reliable Messaging by Graph Transformation Systems}}, BOOKTITLE = {Proc. of the Workshop on Graph Transformation for Verification and Concurrency (GTVC2006)}, EDITOR = {}, SERIES = {}, PUBLISHER = {Elsevier}, NOTE = {}, YEAR = {2006}, URL = {http://www.mit.bme.hu/~gonczy/publications/gtvc2006_gonczy_kovacs_varro.pdf}, ABSTRACT = {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.} }
@INBOOK{Pataricza-Balogh-Gonczy-UML2006, CHAPTER = {{Verification and Validation of Non-functional Aspects in Enterprise Modeling}}, AUTHOR = {Andr{\'a}s Pataricza and Andr{\'a}s Balogh and L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {Enterprise Modeling and Computing with UML}, PUBLISHER = {Idea Group}, NOTE = {}, YEAR = 2006, PAGES = {261-303} }
@INPROCEEDINGS{DECOS-ME06, AUTHOR = {Erwin Schoitsch and Egbert Althammer and Henrik Eriksson and Jonny Vinter and L{\'a}szl{\'o} G{\"o}nczy and Andr{\'a}s Pataricza and Gy{\"o}rgy Csert{\'a}n}, TITLE = {{The DECOS Test Bench - Execution of Verification and Validation Activities and Tool Integration}}, BOOKTITLE = {Proc. of Informationstagung Mikroelektronik ME 2006}, EDITOR = {}, SERIES = {}, PUBLISHER = {}, NOTE = {}, YEAR = {2006}, MONTH = {October 11-12}, ABSTRACT = {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.} }
@INPROCEEDINGS{DECOS-SAFECOMP06, AUTHOR = {Erwin Schoitsch and Egbert Althammer and Henrik Eriksson and Jonny Vinter and L{\'a}szl{\'o} G{\"o}nczy and Andr{\'a}s Pataricza and Gy{\"o}rgy Csert{\'a}n}, TITLE = {{Validation and Certification of Safety-Critical Embedded Systems - the DECOS Test Bench}}, BOOKTITLE = {Proceedings of The 25th International Conference on Computer Safety, Security and Reliability (SAFECOMP2006)}, PAGES = {}, YEAR = {2006}, EDITOR = {}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {Springer}, ADDRESS = {Gdansk, POLAND}, MONTH = {September 25-29}, NOTE = {}, URL = {http://www.mit.bme.hu/~gonczy/publications/safecomp2006.pdf}, ABSTRACT = {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.} }
@INPROCEEDINGS{Gonczy-Varro-WSMATE06, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy and Daniel Varr{\'o}}, TITLE = {{Modeling of Reliable Messaging in Service Oriented Architectures}}, BOOKTITLE = {Proceedings of International Workshop on Web Services Modeling and Testing (WS-MaTe2006)}, PAGES = {35-49}, YEAR = {2006}, EDITOR = {Andrea Polini}, ADDRESS = {Palermo, Sicily, ITALY}, MONTH = {June 9th}, URL = {http://www.mit.bme.hu/~gonczy/publications/Gonczy_WS-MaTe.pdf}, ABSTRACT = {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.} }
@INPROCEEDINGS{Gonczy-CSCS06, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Verification of Reconfiguration Mechanisms in Service-Oriented Architectures}}, BOOKTITLE = {in Proceedings of Conference of PhD Students in Computer Science }, PAGES = {52}, YEAR = {2006}, EDITOR = {}, NOTE = {}, ADDRESS = {Szeged, HUNGARY}, URL = {http://www.mit.bme.hu/~gonczy/publications/gonczy_cscs06.pdf} }
@INPROCEEDINGS{Gonczy-EPEW06, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy and Silvano Chiaradonna and Felicita Di Giandomenico and Andr{\'a}s Pataricza and Andrea Bondavalli and Tam{\'a}s Bartha}, TITLE = {{Dependability Evaluation of Web Service-Based Processes}}, BOOKTITLE = {Proceedings of European Performance Engineering Workshop (EPEW 2006)}, PAGES = {166-180}, YEAR = {2006}, EDITOR = {Mikl{\'o}s Telek}, SERIES = {Lecture Notes on Computer Science}, PUBLISHER = {Springer}, ADDRESS = {Budapest, HUNGARY}, URL = {http://www.springerlink.com/content/ml24537578uw/}, ABSTRACT = {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.} }
@INPROCEEDINGS{Kovacs-Gonczy-GV-VMT06, AUTHOR = {M{\'a}t{\'e} Kov{\'a}cs and L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Simulation and Formal Analysis of Workflow Models}}, BOOKTITLE = {Proc. of the Fifth International Workshop on Graph Transformation and Visual Modeling Techniques}, PAGES = {215-224}, EDITOR = {Roberto Bruni and Daniel Varro}, SERIES = {Electronic Notes in Theoretical Computer Science}, PUBLISHER = {Elsevier}, YEAR = {2006}, ADDRESS = {Vienna, AUSTRIA}, URL = {http://www.mit.bme.hu/~gonczy/publications/gtvmt2006.pdf}, ABSTRACT = {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.} }
@INPROCEEDINGS{Gonczy-Minisym06, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Dependability Analysis and Synthesis of Web Services}}, BOOKTITLE = {Proc. $13^{th}$ PhD Mini-Symposium }, PAGES = {}, YEAR = {2004}, ADDRESS = {Budapest, HUNGARY} }
@INPROCEEDINGS{Gonczy-YR-SOC, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Dependability Analysis of Web Service-based Business Processes by Model Transformations}}, BOOKTITLE = {Proc. of the First European Young Researchers Workshop on Service Oriented Computing (YR-SOC)}, PAGES = {32-37}, EDITOR = {}, YEAR = {2005}, ADDRESS = {Leicester, UK}, URL = {http://www.mit.bme.hu/~gonczy/publications/Gonczy_soc_final.pdf}, ABSTRACT = {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.} }
@INPROCEEDINGS{Gonczy-EDCC, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy and Andr{\'a}s Pataricza and Felicita Di Giandomenico and Silvano Chiaradonna and Andrea Bondavalli}, TITLE = {{Dependability Modeling of Web Service Flows}}, BOOKTITLE = {Supplementary Volume of the Fifth European Conference on Dependable Computing (EDCC-5)}, PAGES = {77-78}, EDITOR = {}, YEAR = {2005}, ADDRESS = {Budapest, HUNGARY}, NOTE = {Fast Abstract} }
@INPROCEEDINGS{Gonczy-Minisym05, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Design of Reliable Web Services}}, BOOKTITLE = {Proc. $12^{th}$ PhD Mini-Symposium }, PAGES = {36-37}, YEAR = {2005}, ADDRESS = {Budapest, HUNGARY} }
@INPROCEEDINGS{Gonczy-CSCS04, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Building Complex Systems of Web Services}}, BOOKTITLE = {Volume of Extended Abtsracts of Conference of PhD Students in Computer Science }, PAGES = {50}, YEAR = {2004}, EDITOR = {}, ADDRESS = {Szeged, HUNGARY} }
@INPROCEEDINGS{Gonczy-FMTU2004, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Web service rendszerek - Systems of Web Services}}, BOOKTITLE = {Fiatal M{\^u}szakiak Tudom{\'a}nyos {\"U}l{\'e}sszaka (FMTU2004)}, PAGES = {105-108}, YEAR = {2004}, NOTE = {In Hungarian}, ADDRESS = {Cluj Napoca, ROMANIA} }
@TECHREPORT{Gonczy-IK, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Katasztr{\'o}fa-elh{\'a}r{\'i}t{\'a}s munkafolyamtokban - Disaster Recovery in Workflows}}, YEAR = {2004}, INSTITUTION = {Budapest University of Technology and Economics} }
@INPROCEEDINGS{Gonczy-Minisym04, AUTHOR = {L{\'a}szl{\'o} G{\"o}nczy}, TITLE = {{Design of Robust Web Services}}, BOOKTITLE = {Proc. $11^{th}$ PhD Mini-Symposium }, PAGES = {42-43}, YEAR = {2004}, ADDRESS = {Budapest, HUNGARY} }
This file has been generated by bibtex2html 1.79