web-archive-it.com » IT » C » CNR.IT

Total: 89

Choose link from "Titles, links and description words view":

Or switch to "Titles and links view".
  • SEFM 2010 - 8th IEEE International Conference on Software Engineering And Formal Methods - Organizing Committee
    Downloads Extras News SEFM 2010 School SEFM Home SEFM 2009 SEFM 2010 Social Event Organizing Committee Chair Patrizia Asirelli ISTI CNR Pisa Italy Maria Luisa Trivella ISTI CNR Pisa Italy Gianluca Trentanni ISTI CNR Pisa Italy Eda Marchetti ISTI CNR

    Original URL path: http://www.sefm2010.isti.cnr.it/committee_organizing.php (2015-08-19)
    Open archived version from archive

  • SEFM 2010 - 8th IEEE International Conference on Software Engineering And Formal Methods - Steering Committee
    School SEFM Home SEFM 2009 SEFM 2010 Social Event Steering Committee Manfred Broy TU Munich Germany Antonio Cerone UNU IIST Macao SAR China Mike Hinchey Lero Limerick Ireland Mathai Joseph TRDDC Pune India Zhiming Liu UNU IIST Macao SAR China

    Original URL path: http://www.sefm2010.isti.cnr.it/committee_steering.php (2015-08-19)
    Open archived version from archive

  • SEFM 2010 - 8th IEEE International Conference on Software Engineering And Formal Methods - Call for Workshops
    METHODS SEFM Pisa Italy 13 18 September 2010 http www sefm2010 isti cnr it SEFM 2010 is the 8th IEEE International Conference on Software Engineering and Formal Methods The aim of the conference is to bring together researchers and practitioners from academia industry and government to advance the state of the art in formal methods to scale up their application in software industry and to encourage their integration with practical engineering methods We invite you to submit proposals for one or two day workshops in the wide area of software engineering and formal methods In particular workshops on challenging new or emerging fields are appreciated SEFM 2010 workshop proposals should include workshop title and brief description of its scope and goals names affiliations and brief CV of the workshop organizers format of the workshop and duration and selection procedure expected number of participants form of proceedings Proposals at most 2 pages should be sent to the workshop chair Maurice ter Beek at The deadline for submissions is 20 January 2010 Notification will be sent by 31 January Workshops with informal proceedings can be assisted in printing and distribution by the SEFM 2010 organizing committee Workshop participants will be offered registration

    Original URL path: http://www.sefm2010.isti.cnr.it/workshops_call.php (2015-08-19)
    Open archived version from archive

  • SEFM 2010 - 8th IEEE International Conference on Software Engineering And Formal Methods - Call for Tutorials
    the state of the art in formal methods to scale up their application in software industry and to encourage their integration with practical engineering methods We invite proposals for full day or half day tutorials related to the topics of SEFM and we encourage tutorials that address recent research themes SEFM 2010 tutorial proposals should include tutorial title names affiliations and brief CV of the tutors duration a description of

    Original URL path: http://www.sefm2010.isti.cnr.it/tutorials_call.php (2015-08-19)
    Open archived version from archive

  • SEFM 2010 - 8th IEEE International Conference on Software Engineering And Formal Methods - Call for Posters
    not limited to Formal techniques and tools to support automated analysis certification debugging learning optimization and transformation of complex systems Case studies and experience reports on industrial applications of formal methods focusing on lessons learned or identification of new research directions Impact of the adoption of formal methods on the development process and associated costs Application of formal methods in standardization and industrial forums Research project overviews Speculative late breaking results Tools Demo Contributions The SEFM 2010 tool demonstrations track provides an opportunity for researchers and practitioners to present and discuss the most recent advances experiences and challenges in the field of Formal Methods with the goal of allowing live presentation of new research tools Tools can range from research prototypes to in house or pre commercialized products There will be a demonstration area open to attendees at scheduled times during the conference during which demonstrators are expected to be available Submission And Publication Submissions must be made electronically through the EasyChair system http www easychair org conferences conf sefm10demos Attached to the poster authors are invited to submit an extended abstract through the workshop paper submission web pages Authors of accepted posters will be expected to present them in person Posters will be displayed during the conference in poster sessions Submissions of proposals for tool demonstrations must describe the technology or approach including references and describe what the expected benefits are of using the tool have an appendix not included in the proceedings but used by the committee to evaluate potential demonstrations that provides a description of how the presentation will be conducted screenshots that may be used in the presentation information on tool availability and maturity and a pointer to a web page for the tool Accepted posters and tool demos presentations will be published in a CNR

    Original URL path: http://www.sefm2010.isti.cnr.it/posters_call.php (2015-08-19)
    Open archived version from archive

  • methods industrial case studies and technology transfer KEYNOTE SPEAKERS Carlo Ghezzi Italy Dimitra Giannakopoulou USA Dusko Pavlovic UK USA LOCATION The conference will be held at the Area della Ricerca CNR Pisa Italy http www area pi cnr it SUBMISSION AND PUBLICATION Submissions to the conference must not have been published or be concurrently considered for publication elsewhere All submissions will be peer reviewed and judged on the basis of originality contribution to the field technical and presentation quality and relevance to the conference All papers must be written in English Research and tool papers must not exceed 10 pages in the IEEE format while short papers must not exceed 5 pages in the IEEE format Instructions for authors are available at http computer org cspress instruct htm LaTeX and MS Word 8 5x11x2 document classes or template can be downloaded from the website at ftp pubftp computer org Press Outgoing proceedings Latex style package ftp pubftp computer org Press Outgoing proceedings IEEE CS Latex8 5x11x2 zip MS Word Template ftp pubftp computer org Press Outgoing proceedings instruct8 5x11x2 doc PDF Instruction file ftp pubftp computer org Press Outgoing proceedings instruct8 5x11x2 pdf All queries on the submissions should be sent to pc chair sefm2010 isti cnr it Papers must be submitted electronically via the Easychair System http www easychair org conferences conf sefm10 The IEEE Computer Society Press will publish the proceedings of the conference Special Issue of FACJ the Formal Aspects of Computing journal will dedicate a special issue to SEFM 2010 for which authors of selected papers will be invited to submit a journal version of their conference paper IMPORTANT DATES Workshop submission deadline 20 January 2010 Title and abstract submission deadline EXTENDED to 29 March 2010 Paper submission deadline EXTENDED to 6 April 2010 Tutorial submission

    Original URL path: http://www.sefm2010.isti.cnr.it/docs/SEFM2010-CFP.txt (2015-08-19)
    Open archived version from archive

  • SEFM 2010 - 8th IEEE International Conference on Software Engineering And Formal Methods - Accepted Papers
    context execution of each method We propose a new algorithm to compute a transition path from the initial state of the system to each error prone transition The computation is carried out using a backward traversal scheme of the FSM support graph where the JPF SE symbolically executes each transition of the path The transition execution performed by JPF SE yields to the backward propagation of the conditions imposed on the input parameters The final section of the paper contains some experimentally results conclusions and suggestions for further work 3 4 Zhiwu Xu Lixiao Zheng and Haiming Chen A Toolkit for Generating Sentences from Context Free Grammars Abstract Click to Show Hide Abstract Producing sentences from a grammar according to various coverage criteria is required in many applications It is also a basic building block for grammar testing which is one of the important techniques for grammar engineering This paper presents a toolkit for context free grammars which mainly consists of several algorithms for sentence generation or enumeration and for coverage analysis for context free grammars The toolkit deals with general context free grammars and is implemented in Java Besides providing implementations of algorithms the toolkit also provides a simple graphical user interface through which the user can use the toolkit directly The toolkit is available at http lcs ios ac cn zhiwu toolkit php In the paper the toolkit and the major algorithms implemented in the toolkit are presented and experimental results are contained Session 04 Formal approaches to service oriented computing 4 1 Natallia Kokash Christian Krause and Erik de Vink Timed Data centric Analysis of Graphical Business Process Models Abstract Click to Show Hide Abstract Reo is a graphical channel based coordination language that enables modeling of complex behavioral protocols using a small set of channel types with well defined behavior Reo has been developed for the coordination of stand alone components or services which makes it suitable for the modeling of service based business processes The existence of formal sematic models for Reo enables computer aided analysis of different aspects of Reo diagrams including their animation simulation control and dataflow verification by means of model checking techniques In this paper we discuss the verification of Reo business process models with mCRL model checking toolset and extend this approach with timed analysis Furthermore we present a detailed example that illustrates the application of Reo and the aforementioned framework to time aware modeling and verification of data centric business processes 4 2 Christian Leuxner Bernd Spanfelner and Wassiou Sitou A formal model for work flows Abstract Click to Show Hide Abstract Within this paper we present a structured formal model for the specification and analysis of work flows The model provides a graphical representation supporting a modular description of work flows together with a formal semantics accurately reflecting the execution of work flows and laying the foundation for tool support Methodically relevant concepts such as hierarchy and refinement are both supported 4 3 Ábel Hegedüs Gábor Bergmann István Ráth and Daniel Varro Back annotation of Simulation Traces with Change Driven Model Transformations Abstract Click to Show Hide Abstract Model driven analysis aims at detecting design flaws early in high level design models by automatically deriving mathematical models These analysis models are subsequently investigated by formal verification and validation V V tools which may retrieve traces violating a certain requirement Back annotation aims at mapping back the results of V V tools to the design model in order to highlight the real source of the fault to ease making necessary amendments Here we propose a technique for the back annotation of simulation traces based on change driven model transformations Simulation traces of analysis models will be persisted as a change model with high level change commands representing macro steps of a trace This trace is back annotated to the design model using change driven transformation rules which bridge the conceptual differences between macro steps in the analysis and design traces Our concepts will be demonstrated on the back annotation problem for analyzing BPEL processes using a Petri net simulator 4 4 Eduardo Mazza Daniel Le Métayer and Maire Laure Potet Designing log architectures for legal evidence Abstract Click to Show Hide Abstract Establishing contractual liabilities in case of litigation is generally a delicate matter It becomes even more challenging when IT systems are involved At the core of the problem lies the issue of the evidence provided by the opposing parties We believe that the means to constitute evidence that could be used in case of conflict should be considered from the onset of IT projects and be part of the requirements for the design of IT systems This paper proposes criteria to characterize acceptable log architectures based on two critical properties observability of events and neutrality of witnesses We show how these criteria depend on the architecture of the system and the potential claims between the parties and propose techniques to enhance a non acceptable log architecture into an acceptable log architecture We illustrate our framework with the case study of a distributed travel booking system with multiple bilateral service agreements Session 05 Applications of formal methods 5 1 Mieke Massink Diego Latella Michael Harrison and Andrea Bracciali A Scalable Fluid Flow Process Algebraic Approach to Emergency Egress Analysis Abstract Click to Show Hide Abstract Pervasive environments offer an increasing number of services to a large number of people moving within these environments including timely information about where to go and when People using these services interact with the system but they are also meeting other people and performing other activities as relevant opportunities arise The design of such systems and the analysis of collective dynamic behaviour of people within them is a challenging problem In previous work we have successfully explored a scalable analysis of stochastic process algebraic models of smart signage systems In this paper we focus on the validation of a representative example of this class of models in the context of emergency egress This context has the advantage that there is detailed data available from studies with alternative analysis methods A second aim is to show how realistic human behaviour often observed in emergency egress can be embedded in the model and how the effect of this behaviour on building evacuation can be analysed in an efficient and scalable way 5 2 Peter Lindsay Kirsten Winter and Nisansala Yatapanage Safety assessment using Behavior Trees and Model Checking Abstract Click to Show Hide Abstract This paper demonstrates the use of Behavior Trees and model checking to assess system safety requirements for a system containing substantial redundancy The case study concerns the hydraulics systems for the Airbus A320 aircraft which are critical for aircraft control The system design is supposed to be able to handle up to 3 different components failing individually without loss of all hydraulic power Verifying the logic of such designs is difficult for humans because of the sheer amount of detail and number of different cases that need to be considered The paper demonstrates how model checking can yield insights into what combinations of component failures can lead to system failure 5 3 Davide Benetti Massimo Merro and Luca Viganò Model Checking Ad Hoc Network Routing Protocols ARAN vs endairA Abstract Click to Show Hide Abstract Several different secure routing protocols have been proposed for determining the appropriate paths on which data should be transmitted in ad hoc networks In this paper we focus on two of the most relevant such protocols ARAN and endairA and present the results of a formal analysis that we have carried out using the AVISPA Tool an automated model checker for the analysis of security protocols By model checking ARAN with the AVISPA Tool we have discovered two attacks a spoofing attack and a disruption one while our analysis of endairA revealed no attacks 5 4 Michael Goldsmith and Sadie Creese Refinement Friendly Bigraphs and Spygraphs Abstract Click to Show Hide Abstract Over the past decade the successful approach to specification and mechanical analysis of correctness and security properties using CSP and its refinement checker FDR has been extended to contexts including mobile ad hoc networks and pervasive systems but the more scope for network reconfiguration the system exhibits the more intricate and less obviously accurate the models must become in order to accommodate such dynamic behaviour in a language with a basically static process and communication graph Milner s Bigraph framework on the other hand and particularly Blackwell s Spygraph specialisation are ideally suited for describing intuitively such dynamic reconfigurations of a system and support notions of locality and adjacency which fits them well for reasoning for instance about the interface between physical and electronic security but they lack powerful analytic tool support Our long term goal is to combine the best of both approaches Unfortunately the canonical labelled transition system induced by the category theoretic semantics of a bigraphical reactive system present a number of challenges to the refinement based approach Prominent amongst these is the feature that the label on a transition is the borrowed context required to make the redex of some reaction rule appear in the augmented source bigraph this means that any reaction which can already take place entirely within a given bigraph gives rise to a transition labelled only with the trivial identity context equivalent to a tau transition in CCS or CSP with the result that neither the reaction rule nor the agents involved can be distinguished This makes it quite impossible for an observer of the transition system to determine whether such a reaction was desirable with respect to any specification We are investigating ways to remedy this situation Here we present a systematic transformation of a bigraphical reactive system both its rules and the underlying bigraphs with the effect that every transition becomes labelled with the specific rule that gave rise to it and the set of agents involved We also consider how that now possibly over precise labelling can be restricted through selective hiding and judicious forgetful renaming Session 06 Model checking 6 1 Maria del Mar Gallardo and David Sanan Verification of Dynamic Data Tree with muCalculus extended with Separation Abstract Click to Show Hide Abstract The problem of verifying software systems that use dynamic data structures such as linked lists queues or binary trees has attracted increasing interest over the last decade Dynamic structures are barely supported by verification techniques because among other reasons it is difficult to efficiently manage the pointer based internal representation This is a key aspect when the goal is to construct a verification tool based on model checking techniques for instance In addition since new nodes may be dynamically inserted or extracted from the structure the shape of the dynamic data and other more specific properties may vary at runtime it being difficult to detect errors such as for instance the non desirable sharing between two nodes In this paper we propose to use muCalculus to describe and analyze by model checking techniques dynamic data such as lists and non linear data structures like trees The expressiveness of mu calculus makes it possible to naturally describe these structures In addition following the ideas of separation logic the logic has been extended with a new operator able to describe the non sharing property which is essential when analyzing data structures of this type 6 2 Jiri Barnat Lubos Brim and Petr Rockai Parallel Partial Order Reduction with Topological Sort Proviso Abstract Click to Show Hide Abstract Partial order reduction and distributed memory processing are two essential techniques to fight the well known state explosion problem in explicit state model checking Unfortunately the two techniques have not been fully satisfactorily combined yet While for verification of safety properties there are rather successful approaches to parallel partial order reduction for full LTL model checking all suggested approaches are either too much technically involved to be smoothly incorporated with the existing parallel algorithms or they are simply weak in the sense that the achieved reduction in the size of the state space is minor The main source of difficulties is the cycle proviso that requires one fully expanded state on every cycle in the reduced state space graph This can be easily achieved in sequential case by employing depth first search strategy for state space generation Unfortunately this strategy is incompatible with parallel hence distributed memory processing which limits application of partial order reduction technique to the sequential case In this paper we suggest a new technique that guarantees correct construction of the reduced state space graph w r t the cycle proviso Our new technique is fully compatible with parallel graph traversal procedure while at the same time it provides competitive reduction of the state space if compared to the serial case The new technique has been implemented within the parallel and distributed memory LTL model checker DiVinE and its performance is reported in this paper 6 3 Franz Weitl Shin Nakajima and Burkhard Freitag Structured Counterexamples for the Temporal Description Logic ALCCTL Abstract Click to Show Hide Abstract A new algorithm for generating counterexamples for the temporal description logic ALCCTL is presented ALCCTL is a decidable combination of the description logic ALC and computation tree logic CTL It extends CTL by unary and binary first order predicates and a restricted form of first order quantification Predicates and quantified expressions are required for representing properties in application domains such as structured web documents and they are frequently used in software and hardware specifications which are verified by model checking In the case of a specification violation existing algorithms generate counterexamples that tend to be complex yet imprecise if specifications contain first order quantified expressions The presented algorithm is the first algorithm for generating counterexamples for a temporal description logic that considers first order predicates and quantification The algorithm is sound and semi complete for ALCCTL The generated counterexamples are both more precise and comprehensible than counterexamples generated by the previous algorithms 6 4 Marcello M Bersani Luca Cavallaro Achille Frigeri Matteo Pradella and Matteo Rossi SMT based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability Abstract Click to Show Hide Abstract An important problem that arises during the execution of service based applications concerns the ability to determine whether a running service can be substituted with one with a different interface for example if the former is no longer available Standard Bounded Model Checking techniques can be used to perform this check but they must be able to provide answers very quickly lest the check hampers the operativeness of the application instead of aiding it The problem becomes even more complex when conversational services are considered i e services that expose operations that have Input Output data dependencies among them In this paper we introduce a formal verification technique for an extension of Linear Temporal Logic that allows users to includein formulae constraints on integer variables This technique applied to the substitutability problem for conversational services is shown to be considerably faster and with smaller memoryfootprint than existing ones Session 07 Formal approaches for testing 7 1 José Pablo Escobedo Christope Gaston Pascale Le Gall and Ana Cavalli Testing Web Service Orchestrators in context a symbolic approach Abstract Click to Show Hide Abstract An orchestrator in a Web service system is a locally deployed piece of software used both to allow users to interact with the system and communicate with remote components Web services in order to fulfill a goal We propose a symbolic model based approach to test orchestrators in the context of the systems they pilot Our approach only takes as input a model of the orchestrator and no models of the Web services In our approach the testing architecture is a parameter communications between Web services and the orchestrator can be either simulated or hidden or observable When they are simulated the orchestrator is tested in isolation and our approach comes to already defined classical model based testing approaches When the SUT is connected with Web services that is in actual usage it is no longer fully controlled by the tester but tested in context In that case two situations may occur either communications with web services are observable or they are hidden Our approach copes with all those cases We give theorems allowing one relating our notion of conformance in context with regard to classical conformance in isolation We present a test case generation algorithm based on symbolic execution techniques it takes into account the status controllable hidden or observable of communication channels between the orchestrator and Web services The algorithm has been implemented and is illustrated on a representative case study 7 2 Maximiliano Cristia Pablo Albertengo and Pablo Rodriguez Monetti Pruning Testing Trees in the Test Template Framework by Detecting Mathematical Contradictions Abstract Click to Show Hide Abstract Fastest is an automatic implementation of Phil Stocks and David Carrington s Test Template Framework TTF a model based testing MBT framework for the Z formal notation In this paper we present a new feature of Fastest that helps TTF users to eliminate inconsistent test classes automatically The method is very simple and practical and makes use of the peculiarities of the TTF Perhaps its most interesting features are extensibility and ease of use since it does not assume previous knowledge on theorem proving Also we compare the solution with a first attempt using the Z EVES proof assistant and with the HOL Z environment At the end we show the results of an empirical assessment based on applying Fastest to four real world industrial strength case studies and to six toy examples 7 3 Peter Gorm Larsen Kenneth Lausdahl and Nick Battle Combinatorial Testing for VDM Abstract Click to Show Hide Abstract Combinatorial testing in VDM involves the automatic generation and execution of a large collection of test cases derived from templates provided in the form of trace definitions added to a VDM specification The main value of

    Original URL path: http://www.sefm2010.isti.cnr.it/program_accepted.php (2015-08-19)
    Open archived version from archive

  • SEFM 2010 - 8th IEEE International Conference on Software Engineering And Formal Methods - Geoff Dromey Biography
    the School of Information and Communication Technology at Griffith University in Brisbane Australia He was the founder and Director of the Software Quality Institute He was a co founder of a successful software company Calytrix Technologies see http www calytrix com which works in the Defence Sector and has offices in Australia and the USA His latest research interests were in development methods that control complexity in the analysis and design of large scale software integrated systems Outcomes of this work over the past ten years have been the Behavior Tree representation and the Behavior Engineering systems analysis and development process see http en wikipedia org wiki Behavior Trees He has authored two books in leading international computer science series Prentice Hall and Addison Wesley and authored co authored more than 50 research journal papers and main conference papers One of his books has sold over 100 000 copies He has been serving on the editorial boards of three international journals Before joining Griffith University he has worked at Stanford University The Australian National University and Wollongong University He has also spent sabbaticals at Oxford University Stanford University and Strathclyde University R Geoff Dromey received a Ph D in chemical

    Original URL path: http://www.sefm2010.isti.cnr.it/geoffDromey.php (2015-08-19)
    Open archived version from archive