2006
Journal article
Unknown
Achieving fault tolerance by a formally validated interaction policy
Fantechi A., Gnesi S., Semini L.
This paper presents the rigorous validation of an integrity policy by means of the application of formal methods and related support tools for its specification and verification. The protocol which carries out the integrity policy is formally specified and formally validated, exploiting model-checking. Specific interaction patterns, which subsume the most complex interaction schemata, are considered and temporal logic formulae expressing the non-violation of integrity rules are checked on them.Source: Lecture notes in computer science (2006): 133–152.
Fantechi A., Gnesi S., Semini L.
This paper presents the rigorous validation of an integrity policy by means of the application of formal methods and related support tools for its specification and verification. The protocol which carries out the integrity policy is formally specified and formally validated, exploiting model-checking. Specific interaction patterns, which subsume the most complex interaction schemata, are considered and temporal logic formulae expressing the non-violation of integrity rules are checked on them.Source: Lecture notes in computer science (2006): 133–152.
See at: CNR ExploRA
2003
Journal 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.
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 ExploRA
2003
Contribution to conference
Open Access
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.DOI: 10.1007/b13229
Metrics:
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.DOI: 10.1007/b13229
Metrics:
See at:
link.springer.com 
| doi.org 
| CNR ExploRA
2008
Contribution to book
Restricted
Software engineering: Ugo Montanari's main contributions and introduction to the section
Gnesi S.
Ugo Montanari began to work in software engineering related topics in the early eighties when he started to promote the use of formal techniques in industries. In that period Ugo established a strong cooperation mainly with Olivetti, that was for more than a decade a very active italian ICT company. Those were also the years when the first Progetto Finalizzato Informatica started and in this contextUgo chaired the P1 subproject, "IndustriaNazionale del settore: Architettura e Struttura dei Sistemi di Elaborazione" whose aims were: i) the development of a prototypical local network meant also to be used to develop software products for the public administration; ii) the realization of a prototypical micro processor with dependability, availability and reconfigurability characteristics to be employed for industrial automation; iii) the development of methods and software programs to be used as basis for the software production.Source: , pp. 258–260, 2008
DOI: 10.1007/978-3-540-68679-8_16
Metrics:
Gnesi S.
Ugo Montanari began to work in software engineering related topics in the early eighties when he started to promote the use of formal techniques in industries. In that period Ugo established a strong cooperation mainly with Olivetti, that was for more than a decade a very active italian ICT company. Those were also the years when the first Progetto Finalizzato Informatica started and in this contextUgo chaired the P1 subproject, "IndustriaNazionale del settore: Architettura e Struttura dei Sistemi di Elaborazione" whose aims were: i) the development of a prototypical local network meant also to be used to develop software products for the public administration; ii) the realization of a prototypical micro processor with dependability, availability and reconfigurability characteristics to be employed for industrial automation; iii) the development of methods and software programs to be used as basis for the software production.Source: , pp. 258–260, 2008
DOI: 10.1007/978-3-540-68679-8_16
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2003
Journal article
Open Access
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.
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:
www.ercim.org | CNR ExploRA
2006
Journal article
Unknown
The industrialization of formal methods
Fitzgerald J. S., Gnesi S., Mandrioli D.
This special section contains papers based on work presented at the 12th International Symposium on Formal Methods (FM 2003) held at the CNR Research Campus in Pisa on 8-13 September 2003. The papers all focus on tools and techniques for cost-effective application of formal methods on the industrial scale. The papers discuss a range of approaches, including the development of domain-specific and general-purpose techniques, and the construction of suites of cooperating but specialised tools. In spite of the diversity of approach, the papers share some themes, notably the levels of automation that are possible at appropriate levels of abstraction, and the incorporation of formal techniques within existing development paradigms. Although three papers cannot provide a comprehensive view, they do provide a useful 'snapshot' of dominant concerns in industrial-strength formal methods today.Source: International journal on software tools for technology transfer (Internet) 8 (2006): 301–302.
Fitzgerald J. S., Gnesi S., Mandrioli D.
This special section contains papers based on work presented at the 12th International Symposium on Formal Methods (FM 2003) held at the CNR Research Campus in Pisa on 8-13 September 2003. The papers all focus on tools and techniques for cost-effective application of formal methods on the industrial scale. The papers discuss a range of approaches, including the development of domain-specific and general-purpose techniques, and the construction of suites of cooperating but specialised tools. In spite of the diversity of approach, the papers share some themes, notably the levels of automation that are possible at appropriate levels of abstraction, and the incorporation of formal techniques within existing development paradigms. Although three papers cannot provide a comprehensive view, they do provide a useful 'snapshot' of dominant concerns in industrial-strength formal methods today.Source: International journal on software tools for technology transfer (Internet) 8 (2006): 301–302.
See at: CNR ExploRA
2003
Journal article
Open Access
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
Metrics:
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
Metrics:
See at:
doi.org | www.elsevier.nl | CNR ExploRA
2002
Contribution to conference
Unknown
Application of Linguistic Techniques for Requirements Analysis
Gnesi S.
An abstract is not availableSource: FM&&T Day, Pisa, Italy, 2002
Gnesi S.
An abstract is not availableSource: FM&&T Day, Pisa, Italy, 2002
See at: CNR ExploRA
2010
Contribution to conference
Restricted
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
Metrics:
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
Metrics:
See at:
doi.org | ieeexplore.ieee.org | CNR ExploRA
2003
Contribution to journal
Open Access
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).DOI: 10.1016/s0167-6423(02)00091-6
Metrics:
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).DOI: 10.1016/s0167-6423(02)00091-6
Metrics:
See at:
doi.org | www.sciencedirect.com | CNR ExploRA
2003
Report
Unknown
A model checking verification environment for mobile systems
Ferrari G., Gnesi S., Montanari U., Pistore M.
In this paper a semantic-based environment for reasoning about the behaviour of mobile systems is presented. The verification environment, called HAL, exploits a novel automata-like model which allows finite state verification of systems specified in the pi-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 with some case studiesSource: ISTI Technical reports, 2003
Ferrari G., Gnesi S., Montanari U., Pistore M.
In this paper a semantic-based environment for reasoning about the behaviour of mobile systems is presented. The verification environment, called HAL, exploits a novel automata-like model which allows finite state verification of systems specified in the pi-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 with some case studiesSource: ISTI Technical reports, 2003
See at: CNR ExploRA
2006
Contribution to conference
Unknown
Preface. First International Workshop on Software Certification
Gnesi S., Maibaum T., Wassyng A.
Software is currently used to control medical devices, automobiles, aircraft, manufacturing plants, nuclear generating stations, space exploration systems, elevators, electric motors, automated trains, banking transactions, telecommunications devices and a growing number of devices in industry and in our homes. Software is also mission critical for many organizations, even if the software does not 'control' what happens. Clearly, many of these systems have the potential to cause physical harm if they malfunction. Even if they do not cause physical harm, their malfunctions are capable of causing financial and political chaos. Currently there is no consistent regulation of software and society is starting to demand that software used in critical systems must meet minimum safety, security and reliability standards. Manufacturers of these systems are in the unenviable position of not having any clear guidelines as to what may be regarded as acceptable standards in these situations. Even where the systems are not mission critical, software producers and their customers are becoming interested in methods for assuring quality that may result in software supplied with guarantees. The purpose of the workshop is to discuss issues related to software certification.
Gnesi S., Maibaum T., Wassyng A.
Software is currently used to control medical devices, automobiles, aircraft, manufacturing plants, nuclear generating stations, space exploration systems, elevators, electric motors, automated trains, banking transactions, telecommunications devices and a growing number of devices in industry and in our homes. Software is also mission critical for many organizations, even if the software does not 'control' what happens. Clearly, many of these systems have the potential to cause physical harm if they malfunction. Even if they do not cause physical harm, their malfunctions are capable of causing financial and political chaos. Currently there is no consistent regulation of software and society is starting to demand that software used in critical systems must meet minimum safety, security and reliability standards. Manufacturers of these systems are in the unenviable position of not having any clear guidelines as to what may be regarded as acceptable standards in these situations. Even where the systems are not mission critical, software producers and their customers are becoming interested in methods for assuring quality that may result in software supplied with guarantees. The purpose of the workshop is to discuss issues related to software certification.
See at: CNR ExploRA
2008
Contribution to book
Restricted
Graph-based design and analysis of dynamic software architectures
Bucchiarone A., Gnesi S., Bruni R., Lafuente A. L., Hirsch D.
We illustrate two ways to address the specification, modelling and analysis of dynamic software architectures using: i) ordinary typed graph transformation techniques implemented in Alloy; ii) a process algebraic presentation of graph transformation implemented in Maude. The two approaches are compared by showing how different aspects can be tackled, including representation issues, modelling phases, property specification and analysis.Source: Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, edited by Pierpaolo Degano; Rocco De Nicola; Josè Meseguer, pp. 37–56. Berlin: Springer Berlin / Heildelberg, 2008
DOI: 10.1007/978-3-540-68679-8_4
Metrics:
Bucchiarone A., Gnesi S., Bruni R., Lafuente A. L., Hirsch D.
We illustrate two ways to address the specification, modelling and analysis of dynamic software architectures using: i) ordinary typed graph transformation techniques implemented in Alloy; ii) a process algebraic presentation of graph transformation implemented in Maude. The two approaches are compared by showing how different aspects can be tackled, including representation issues, modelling phases, property specification and analysis.Source: Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, edited by Pierpaolo Degano; Rocco De Nicola; Josè Meseguer, pp. 37–56. Berlin: Springer Berlin / Heildelberg, 2008
DOI: 10.1007/978-3-540-68679-8_4
Metrics:
See at:
doi.org | CNR ExploRA
2006
Contribution to book
Closed Access
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
Metrics:
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
Metrics:
See at:
doi.org | CNR ExploRA
2005
Conference article
Open Access
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
Metrics:
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
Metrics:
See at:
doi.org | link.springer.com | NARCIS | NARCIS | NARCIS | NARCIS | www.scopus.com | www.springerlink.com | CNR ExploRA
2011
Journal article
Restricted
Model Checking : cos'è e come si applica
Alessandro Fantechi, Stefania Gnesi
Il model checking ha dimostrato di essere una tecnologia di successo per verificare la correttezza dei requisiti nella progettazione di un consistente numero di sistemi real-time, embedded e safety-critical. Lo scopo di questo breve articolo è di spiegare come funziona.Source: Mondo Digitale 38-39 (2011): 29–38.
Alessandro Fantechi, Stefania Gnesi
Il model checking ha dimostrato di essere una tecnologia di successo per verificare la correttezza dei requisiti nella progettazione di un consistente numero di sistemi real-time, embedded e safety-critical. Lo scopo di questo breve articolo è di spiegare come funziona.Source: Mondo Digitale 38-39 (2011): 29–38.
See at:
www.mondodigitale.net | CNR ExploRA
2011
Contribution to book
Restricted
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
Metrics:
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
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2011
Contribution to book
Open Access
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
Metrics:
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
Metrics:
See at:
eprints.imtlucca.it | doi.org | link.springer.com | CNR ExploRA
2011
Contribution to book
Restricted
Specification and implementation of demonstrators for the case studies
Elgner J., Gnesi S., Koch N., Mayer P.
A main challenge in Sensoria has been the inclusion of case studies from different industrial and academic application areas, namely finance, automotive, telecommunications, and university administration. The case studies, along with a short description of available scenarios, have already been introduced in Chapter 0-3. In this chapter, we go into more detail, presenting the (graphical) specifications for selected scenarios by using the modeling approaches introduced in Sensoria. Furthermore, we detail the implementation of demonstrators for some of the case studies.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ölz, pp. 640–654. Berlin/Heidelberg: Springer-Verlag, 2011
DOI: 10.1007/978-3-642-20401-2_31
Project(s): SENSORIA
Metrics:
Elgner J., Gnesi S., Koch N., Mayer P.
A main challenge in Sensoria has been the inclusion of case studies from different industrial and academic application areas, namely finance, automotive, telecommunications, and university administration. The case studies, along with a short description of available scenarios, have already been introduced in Chapter 0-3. In this chapter, we go into more detail, presenting the (graphical) specifications for selected scenarios by using the modeling approaches introduced in Sensoria. Furthermore, we detail the implementation of demonstrators for some of the case studies.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ölz, pp. 640–654. Berlin/Heidelberg: Springer-Verlag, 2011
DOI: 10.1007/978-3-642-20401-2_31
Project(s): SENSORIA
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2012
Contribution to conference
Restricted
Foreward - VaMoS '12
Eisenecker U. W., Apel S., Gnesi S.
This volume contains the proceedings of the Sixth International Workshop on Variability Modelling of Software-intensive Systems (VaMoS 2012), January 25-28, 2012, hosted by the Faculty of Economics and Management Science of the University of Leipzig, Germany. The aim of the VaMoS workshop series is to bring together researchers from various 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. The Program Committee of VaMoS 2012 received 43 submissions. We would like to thank all authors for submitting their papers. Each paper was reviewed by at least three reviewers. Based on the review reports and intensive discussions conducted electronically, the Program Committee selected 22 regular papers (acceptance rate around 51%). We would like to thank the Program Committee members and all reviewers for their efforts in the selection process. In addition to contributed papers, the conference program includes two keynotes. We are grateful to Paulo Borba, Centro de Informatica, Universidade Federal de Pernambuco, Brasil and Charles Krueger, BigLever Software, USA for accepting our invitation to address the workshop. We also would like to thank the members of the Steering Committee, the Organizing Committee, as well as several other people whose efforts contributed to make the workshop a success. VaMoS 2012 is sponsored by the ACM, and received support of the several industrial sponsors.Source: New York: ACM, Association for computing machinery, 2012
Eisenecker U. W., Apel S., Gnesi S.
This volume contains the proceedings of the Sixth International Workshop on Variability Modelling of Software-intensive Systems (VaMoS 2012), January 25-28, 2012, hosted by the Faculty of Economics and Management Science of the University of Leipzig, Germany. The aim of the VaMoS workshop series is to bring together researchers from various 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. The Program Committee of VaMoS 2012 received 43 submissions. We would like to thank all authors for submitting their papers. Each paper was reviewed by at least three reviewers. Based on the review reports and intensive discussions conducted electronically, the Program Committee selected 22 regular papers (acceptance rate around 51%). We would like to thank the Program Committee members and all reviewers for their efforts in the selection process. In addition to contributed papers, the conference program includes two keynotes. We are grateful to Paulo Borba, Centro de Informatica, Universidade Federal de Pernambuco, Brasil and Charles Krueger, BigLever Software, USA for accepting our invitation to address the workshop. We also would like to thank the members of the Steering Committee, the Organizing Committee, as well as several other people whose efforts contributed to make the workshop a success. VaMoS 2012 is sponsored by the ACM, and received support of the several industrial sponsors.Source: New York: ACM, Association for computing machinery, 2012
See at:
dl.acm.org | CNR ExploRA