Found 282 result(s)
Found 15 page(s)
Page Size: 10, 20, 50
Export: bibtex, xml, json, csv

2003 Book Open Access OPEN

Special issue on the Fifth International Workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems
Garavel H., Gnesi S., Schieferdeckerc I.
The purpose of this special issue of the International Journal Science in Computer Programming is to present a selection of papers from the Proceedings of the 5th ERCIM International Workshop on Formal Methods for Industrial Critical Systems (FMICS), which took place in Berlin in March 2000. FMICS is the ERCIM Working Group on Formal Methods for Industrial Critical Systems. Launched in 1996 by Diego Latella and Stefania Gnesi (CNR Pisa), the FMICS working group is currently chaired by Hubert Garavel (INRIA Rhone-Alpes).Source: info:cnr-pdr/source/autori:Garavel H.; Gnesi S.; Schieferdeckerc I./titolo:Special issue on the Fifth International Workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems/editore:/anno:2003
DOI: 10.1016/S0167-6423(02)00091-6

See at: BASE (Open Access Aggregator) Open Access | DOI Resolver | CNR People | www.sciencedirect.com


2003 Article Unknown

A model-checking verification environment for mobile processes
Ferrari G. L., Gnesi S., Montanari U., Pistore M.
This article presents a semantic-based environment for reasoning about the behavior of mobile systems. The verification environment, called HAL, exploits a novel automata-like model that allows finite-state verification of systems specified in the ?-calculus. The HAL system is able to interface with several efficient toolkits (e.g. model-checkers) to determine whether or not certain properties hold for a given specification. We report experimental results on some case studies.Source: ACM transactions on software engineering and methodology 12 (2003): 440–473.

See at: CNR People


2014 Book Unknown

2nd FME Workshop on Formal Methods in Software Engineering
Gnesi S., Plat N.
The proceedings contain 9 papers. The topics discussed include: using mCRL2 for the analysis of software product lines; flexible modular formalization of UML sequence diagrams; formal specification comprehension; software reliability via machine learning; compiling polychronous programs into conditional partial orders for ASIP synthesis; from an abstract specification in event-B toward an UML/OCL model; generating supportive hypotheses in introducing formal methods using a software processes improvement model; formalization of software models for cyber-physical; and analysis and testing of PLEXIL plans.Source: New York: ACM Press, 2014

See at: dl.acm.org | CNR People


2003 Article Unknown

Model checking of embedded systems
Gnesi S.
The integration of different dependability techniques is an open research question. We address problems that arise when attempting to combine fault tolerance mechanisms with formal methods and formal verification tools in the development of an embedded system.Source: ERCIM news 52 (2003): 37–38.

See at: CNR People | www.ercim.org


2016 Book Unknown

FM 2016 - Formal Methods. 21st International Symposium
Gnesi S., Fitzgerald J. S., Heitmeyer C. L., Philippou A.
The 2016 symposium received 162 submissions to the main track - the largest number of contributions to a regular symposium in the FM series to date. Review of each submission by at least three Program Committee members followed by a dis- cussion phase led to the selection of 43 papers - an acceptance rate of 0.265. These proceedings also contain six papers selected by the Program Committee of the Industry Track chaired by Georgia Kapitsaki (University of Cyprus), Tiziana Margaria (University of Limerick and Lero, Ireland), and Marcel Verhoef (European Space Agency, The Netherlands).Source: info:cnr-pdr/source/autori:Gnesi S.; Fitzgerald J. S.; Heitmeyer C. L.; Philippou A.; (eds.)/titolo:FM 2016 - Formal Methods. 21st International Symposium/editore:/anno:2016
DOI: 10.1007/978-3-319-48989-6

See at: DOI Resolver | link.springer.com | CNR People


2013 Book Unknown

The Seventh International Workshop on Variability Modelling of Software-intensive Systems
Gnesi S., Collet P., Schmid K.
This volume contains the proceedings of the Seventh International Workshop on Variability Modelling of Software-intensive Systems (VaMoS 2013), 23-25 January 2013, hosted by the ISTI-CNR, Pisa, Italy. Previous editions were held in Leipzig (2012), Namur (2011), Linz (2010), Sevilla (2009), Essen (2008) and Limerick (2007). The VaMoS workshop series aims at bringing together researchers from different areas dedicated to mastering variability to discuss advantages, drawbacks, and complementarities of various approaches and to present new results for mastering variability throughout the whole life cycle of systems, system families, and product lines. VaMoS has always been a highly interactive event that is one of the major venues of the variability modelling community, where most of the core researchers in the field meet and exchange ideas. codice puma: cnr.isti/2013-ED-006Source: New York: ACM Press, 2013

See at: dl.acm.org | CNR People


2015 Book Open Access OPEN

Proceedings FMSPLE 2015
Gnesi S., Atlee J. M.
The workshop aims at reviewing the state of the art and the state of the practice in which formal methods and analysis approaches are currently applied in SPLE. This leads to a discussion of a research agenda for the extension of existing formal approaches and the development of new formal techniques for dealing with the particular needs of SPLE. To achieve the above objectives, the workshop is intended as a highly interactive event fostering discussion and initiating collaborations between the participants from both communities.Source: info:cnr-pdr/source/autori:Gnesi S.; Atlee J. M./titolo:Proceedings FMSPLE 2015/editore:/anno:2015
DOI: 10.4204/EPTCS.182

See at: arXiv.org e-Print Archive Open Access | arxiv.org | DOI Resolver | CNR People


2013 Book Unknown

17th International Software Product Line Conference
Gnesi S., Kishi T., Jarzabek S.
Welcome to SPLC 2013, the 17th International Software Product Line Conference. SPLC is the premier forum for practitioners, researchers to present and discus ideas, research results and experiences as well as issues and problems in the field. The program consists of a broad combination of keynotes, research and industry papers, panels, tutorials, workshops, tools and demos, the doctoral symposium and Product Line Hall of Fame.Source: New York: ACM Press, 2013

See at: dl.acm.org | CNR People


2002 Conference object Unknown

Application of Linguistic Techniques for Requirements Analysis
Gnesi S.
No abstract available.Source: FM&&T Day, Pisa, Italy, 2002

See at: CNR People


2010 Book Unknown

Preface of SEFM 2010
Fiadeiro J., Gnesi S., Maggiolo Schettini A.
This volume contains the proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010) held on 13-18 September 2010 in Pisa, Italy, hosted by the Istituto di Scienza e Tecnologie dell'Informazione A. Faedo of the Consiglio Nazionale delle Ricerche (ISTI-CNR).Source: New York: IEEE, Institute of electrical and electronics engineers, 2010
DOI: 10.1109/SEFM.2010.5

See at: DOI Resolver | ieeexplore.ieee.org | CNR People


2015 Article Unknown

Special section on the 17th International Software Product Line Conference
Gnesi S., Jarzabek S.
Today, companies develop, maintain and deploy families of similar software products (e.g., games for different models of smartphones) rather than a single product. Software product lines engineering refers to software engineering methods, tools and techniques for creating a collection of similar software systems from a shared set of software assets using a common means of production. Software Product Line Conferences started in 1996, as the premier forum for practitioners, researchers and educators to present and discuss the most recent ideas, innovations, trends, experiences, and concerns in the area of software product lines, software product family engineering and, more recently, systems family engineering, managing families of software products as a whole rather than each family member individually. This special section stems from the 17th SPL Conference held in Tokyo, Japan, in August 2013. The contributions to this special section are further elaborations of the papers presented at the conference.Source: International journal on software tools for technology transfer (Print) 17 (2015): 555–557. doi:10.1007/s10009-015-0386-x
DOI: 10.1007/s10009-015-0386-x

See at: DOI Resolver | link.springer.com | CNR People


2003 Article Open Access OPEN

Formal specification and verification of complex systems
Gnesi S.
The application of formal methods in the rigorous de nition and analysis of the functionality and the behaviour of a system, promises the ability of showing that the system is correct. Given such a promise, that is already out since several years, it is astonishing to see how little formal methods are actually used in the safety critical system industry, though the use of formal methods is increasingly required by the international standards and guidelines for the development of complex systems.Source: Electronic notes in theoretical computer science 80 (2003): 1–5. doi:10.1016/S1571-0661(04)80829-6
DOI: 10.1016/S1571-0661(04)80829-6

See at: BASE (Open Access Aggregator) Open Access | DOI Resolver | CNR People | www.elsevier.nl


2012 Article Unknown

Editorial in Formal Aspects of Computing
Fiadeiro J. L., Gnesi S., Maibaum T.
Source: Formal aspects of computing 24 (2012): 161–162. doi:10.1007/s00165-012-0224-9
DOI: 10.1007/s00165-012-0224-9

See at: DOI Resolver | link.springer.com | CNR People


2011 Part of book or chapter of book Unknown

Introduction to the Sensoria Case Studies
Elgner J., Gnesi S., Koch N., Mayer P.
The foundational research carried out in Sensoria has been steered by a number of case studies for ensuring applicability of Sensoria methods and meeting expectations of society and the economy. In this chapter, we introduce these case studies. Three of the case studies came from industrial applications in automotive, finance and telecommunication domains; one came from an academic application for distributed e-learning and course management. Having in mind the relevance that these areas have in society and the economy, the above case studies have been extensively used in Sensoria during the whole project.Source: Rigorous Software Engineering for Service-Oriented Systems. Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing, edited by Wirsing, Martin ; Hölzl, Matthias, pp. 26–34. Berlin: Springer-Verlag, 2011
DOI: 10.1007/978-3-642-20401-2_3
Project(s): SENSORIA

See at: DOI Resolver | link.springer.com | CNR People


2003 Article Unknown

Preface - Special issue on the Fifth International Workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems, Berlin, April 3-4, 2000--selected papers
Garavel H., Gnesi S., Schieferdecker I.
The purpose of this special issue of the International Journal Science in Computer Programming is to present a selection of papers from the Proceedings of the 5th ERCIM International Workshop on Formal Methods for Industrial Critical Systems (FMICS), which took place in Berlin in March 2000. FMICS is the ERCIM Working Group on Formal Methods for Industrial Critical Systems. Launched in 1996 by Diego Latella and Stefania Gnesi (CNR Pisa), the FMICS working group is currently chaired by Hubert Garavel (INRIA Rhone-Alpes).Source: Science of computer programming (Print) 46 (2003): 145–146.

See at: CNR People | www.sciencedirect.com


2013 Part of book or chapter of book Unknown

Families of dependable systems:a model checking approach
Gnesi S.
A number of models, logics and associated tools for the qualitative analysis of variability aspects and their use to deal with adaptability and evolvability of systems have recently been proposed. In these lectures, we will introduce the action-based branching-time temporal logic MHML which allows expressing constraints over the products of a family as well as constraints over their behaviour in a single logical framework. Based on model-checking techniques for MHML, a modelling and verification framework will be presented that can automatically generate all the valid productsof the family, visualise the family/products behaviour and efficiently model check properties expressed in MHML over products and families alike. The use of the above methods, techniques and tools will be applied to a scenario derived from a family of dependable systems.Source: Engineering Dependable Software Systems, edited by Broy M., Peled D., Kalus G., pp. 115–140, 2013

See at: CNR People | www.iospress.nl


2005 Conference object Unknown

A formal security analysis of an OSA/Parlay authentication interface
Corin R., Di Caprio G., Etalle S., Gnesi S., Lenzini G., Moiso C.
We report on an experience in analyzing the security of the Trust and Security Management (TSM) protocol, an authentication procedure within the OSA/Parlay Application Program Interfaces (APIs) of the Open Service Access and Parlay Group. The experience has been conducted jointly by research institutes experienced in security and industry experts in telecommunication networking. OSA/Parlay APIs are designed to enable the creation of telecommunication applications outside the traditional network space and business model. Network operators consider the OSA/Parlay a promising architecture to stimulate the development of web service applications by third party providers, which may not necessarily be experts in telecommunication and security. The TSM protocol is executed by the gateways to OSA/Parlay networks; its role is to authenticate client applications trying to access the interfaces of some object representing an offered network capability. For this reason, potential security flaws in the TSM authentication strategy can cause the unauthorized use of the network, with evident damages to the operator and the quality of services. We report a rigorous formal analysis of the TSM specification, which is originally given in UML. Furthermore, we illustrate our design choices to obtain the formal model, describe the tool-aided verification and finally expose the security flaws discovered.Source: 7th International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 131–146, Athens, GREECE, JUN 15-17, 2005
DOI: 10.1007/11494881_9

See at: DOI Resolver | CNR People | www.springerlink.com


2006 Part of book or chapter of book Unknown

Achieving Fault Tolerance by a Formally Validated Interaction Policy
Alessandro Fantechi, Stefania Gnesi, Laura Semini
This paper addresses the rigorous validation of an integrity policy by means of the application of formal methods and related support tools. We show how the policy, which provides a flexible fault tolerant schema, can be specified using a process algebra and verified using model checking techniques. Actually, we show how this approach allows both the generic validation of a middleware based on such integrity policy, and the validation of an integrated application which internally uses this mechanism. In the first case, the fault tolerance of a system, possibly composed of Commercial Off The Shelf (COTS) components, is guaranteed by a validated resident interaction control middleware. The second case applies instead when the application is forced to use a given middleware, as it is the case of Web Services.Source: Rigorous Development of Complex Fault-Tolerant Systems, edited by Michael J. Butler; ;Cliff B. Jones;Alexander Romanovsky;Elena Troubitsyna, pp. 133–152. Berlin: Springer Berlin / Heildelberg, 2006
DOI: 10.1007/11916246_7

See at: DOI Resolver | CNR People


2003 Book Unknown

FME 2003: Formal Methods
Araki K., Gnesi S., Mandrioli D.
This volume contains the proceedings of FM 2003, the 12th International Formal Methods Europe Symposium which was held in Pisa, Italy on September 8 14, 2003. Formal Methods Europe (FME, www.fmeurope.org) is an independent association which aims to stimulate the use of and research on formal methods for system development. FME conferences began with a VDM Europe symposium in 1987. Since then, the meetings have grown and have been held about once every 18 months. Throughout the years the symposia have been notably successful in bringing together researchers, tool developers, vendors, and users, both from academia and from industry. Unlike previous symposia in the series, FM 2003 was not given a speci c theme. Rather, its main goal could be synthesized as widening the scope. Indeed, the organizers aimed at enlarging the audience and impact of the symposium along several directions. Dropping the su x E from the title of the conference re ects the wish to welcome participation and contribution from every country; also, contributions from outside the traditional Formal Methods community were solicited. The recent innovation of including an Industrial Day as an important part of the symposium shows the strong commitment to involve industrial people more and more within the Formal Methods community.Source: info:cnr-pdr/source/autori:Araki K.; Gnesi S.; Mandrioli D./titolo:FME 2003: Formal Methods/editore:/anno:2003
DOI: 10.1007/b13229

See at: DOI Resolver | link.springer.com | CNR People


2011 Part of book or chapter of book Unknown

The Sensoria approach applied to the finance case study
Gnesi S., Pugliese R., Tiezzi F.
This chapter provides an effective implementation of (part of) the Sensoria approach, specifically modelling and formal analysis of service-oriented software based on mathematically founded techniques. The 'Finance case study' is used as a test bed for demonstrating the feasibility and effectiveness of the use of the process calculus COWS and some of its related analysis techniques and tools. In particular, we report the results of an application of a temporal logic and its model checker for expressing and checking functional properties of services and a type system for guaranteeing confidentiality properties of services.Source: Rigorous Software Engineering for Service-Oriented Systems. Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing, edited by Martin Wirsing, Matthias Hölzl, pp. 698–718. Berlin: Springer-Verlag, 2011
DOI: 10.1007/978-3-642-20401-2_34
Project(s): SENSORIA

See at: DOI Resolver | link.springer.com | CNR People