Search For:

Displaying 1-21 out of 21 total
Model-Based Development and Formal Methods in the Railway Industry
Found in: IEEE Software
By Alessio Ferrari,Alessandro Fantechi,Stefania Gnesi,Gianluca Magnani
Issue Date:May 2013
pp. 28-34
The transition from a code-based process to a model-based process isn't easy. This is particularly true for a company that operates in a safety-critical sector, where the products must be developed according to international standards, with certified tools...
 
Using collective intelligence to detect pragmatic ambiguities
Found in: 2012 IEEE 20th International Requirements Engineering Conference (RE)
By Alessio Ferrari,Stefania Gnesi
Issue Date:September 2012
pp. 191-200
This paper presents a novel approach for pragmatic ambiguity detection in natural language (NL) requirements specifications defined for a specific application domain. Starting from a requirements specification, we use a Web-search engine to retrieve a set ...
 
Formal Description of Variability in Product Families
Found in: Software Product Line Conference, International
By Patrizia Asirelli,Maurice H. ter Beek,Stefania Gnesi,Alessandro Fantechi
Issue Date:August 2011
pp. 130-139
We illustrate how to manage variability in a single logical framework consisting of a Modal Transition System (MTS) and an associated set of formulae expressed in the branching-time temporal logic MHML interpreted in a deontic way over such MTSs. We discus...
 
Variability and Rigour in Service Computing Engineering
Found in: Software Engineering Workshop, Annual IEEE/NASA Goddard
By Maurice H. ter Beek,Stefania Gnesi,Alessandro Fantechi,José L. Fiadeiro
Issue Date:June 2011
pp. 122-127
We present a research agenda on an emerging topic in software engineering, namely the synergy between Software Product Line Engineering (SPLE) and Service-Oriented Computing (SOC). Our proposal is to develop rigorous modelling techniques as well as analysi...
 
An Approach to Ambiguity Analysis in Safety-Related Standards
Found in: Quality of Information and Communications Technology, International Conference on the
By Isabella Biscoglio, Alessandro Coco, Mario Fusani, Stefania Gnesi, Gianluca Trentanni
Issue Date:October 2010
pp. 461-466
Standards for systems and software lifecycle processes have become rather popular in the last decade. Being expressed in natural language, their requirements, or clauses, are exposed to the risk of ambiguity, vagueness and subjectivity, even when safety of...
 
Formal verification of an automotive scenario in service-oriented computing
Found in: Software Engineering, International Conference on
By Maurice ter Beek, Stefania Gnesi, Nora Koch, Franco Mazzanti
Issue Date:May 2008
pp. 613-622
We report on the successful application of academic experience with formal modelling and verification techniques to an automotive scenario from the service-oriented computing domain. The aim of this industrial case study is to verify a priori, thus before ...
 
Controlling Requirements Evolution: a Formal Concept Analysis-Based Approach
Found in: Software Engineering Advances, International Conference on
By Fabrizio Fabbrini, Mario Fusani, Stefania Gnesi, Giuseppe Lami
Issue Date:August 2007
pp. 68
Requirements evolve during the software development process. Requirements specification evolution determines changes both in terms of level of details and style of representation and it brings the requirements from the initial statement of the customer nee...
 
Web Service Composition Approaches: From Industrial Standards to Formal Methods
Found in: Internet and Web Applications and Services, International Conference on
By Maurice ter Beek, Antonio Bucchiarone, Stefania Gnesi
Issue Date:May 2007
pp. 15
Composition of web services is much studied to support business-to-business and enterprise application integration in e-Commerce. Current web service composition approaches range from practical languages aspiring to become standards (like BPEL, WS-CDL, OWL...
 
Formal Modelling and Verification of an Asynchronous Extension of SOAP
Found in: Web Services, European Conference on
By Maurice H. ter Beek, Stefania Gnesi, Franco Mazzanti, Corrado Moiso
Issue Date:December 2006
pp. 287-296
Current web services are largely based on a synchronous request-response model that uses the Simple Object Access Protocol SOAP. Next-generation telecommunication networks, on the contrary, are characterised by the need to handle asynchronous interactions ...
 
Formal Test-Case Generation for UML Statecharts
Found in: Engineering of Complex Computer Systems, IEEE International Conference on
By Stefania Gnesi, Diego Latella, Mieke Massink
Issue Date:April 2004
pp. 75-84
The Unified Modeling Language has been introduced as a notation for modeling and reasoning about large and complex systems, and their design, across a wide range of application domains. System modeling and analysis techniques, especially those based on for...
 
Model Checking UML Statechart Diagrams Using JACK
Found in: High-Assurance Systems Engineering, IEEE International Symposium on
By Stefania Gnesi, Diego Latella, Mieke Massink
Issue Date:November 1999
pp. 46
Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modeling Language (UML). In this paper we present a branching time model-checking approach to the automatic verification of formal correc...
 
Formal Modeling for Product Families Engineering
Found in: Software Product Line Conference, International
By Alessandro Fantechi, Stefania Gnesi
Issue Date:September 2008
pp. 193-202
In this paper we propose a behavioural model, namely the Generalized Extended Modal Transition Systems, as a basis for the formalization of different notions of variability usually present in??product families definitions. In particular, a GEMTS is able to...
 
Demonstration of a model checker for the analysis of product variability
Found in: Proceedings of the 16th International Software Product Line Conference - Volume 2 (SPLC '12)
By Franco Mazzanti, Maurice H. ter Beek, Stefania Gnesi
Issue Date:September 2012
pp. 242-245
We demonstrate an experimental tool for the modeling and analysis of behavioral variability in product families.
     
Towards an executable algebra for product lines
Found in: Proceedings of the 16th International Software Product Line Conference - Volume 2 (SPLC '12)
By Marinella Petrocchi, Stefania Gnesi
Issue Date:September 2012
pp. 66-73
We propose the Controlled Language for Software Product Lines CL4SPL with the twofold aim of ensuring simplicity of use for product line engineers and safe translations to executable languages amenable for automated verification. We show an implementation ...
     
A logical verification methodology for service-oriented computing
Found in: ACM Transactions on Software Engineering and Methodology (TOSEM)
By Alessandro Fantechi, Alessandro Lapadula, Francesco Tiezzi, Franco Mazzanti, Rosario Pugliese, Stefania Gnesi
Issue Date:June 2012
pp. 1-46
We introduce a logical verification methodology for checking behavioral properties of service-oriented computing systems. Service properties are described by means of SocL, a branching-time temporal logic that we have specifically designed for expressing i...
     
Design and validation of variability in product lines
Found in: Proceeding of the 2nd international workshop on Product line approaches in software engineering (PLEASE '11)
By Alessandro Fantechi, Franco Mazzanti, Maurice H. ter Beek, Patrizia Asirelli, Stefania Gnesi
Issue Date:May 2011
pp. 25-30
We propose an emerging solution technique, pushing the application of model-checking techniques to the design and validation of variability in a product line (PL), mainly aimed at those industrial domains where model-based development is adopted for the de...
     
CMC-UMC: a framework for the verification of abstract service-oriented properties
Found in: Proceedings of the 2009 ACM symposium on Applied Computing (SAC '09)
By Franco Mazzanti, Maurice H. ter Beek, Stefania Gnesi
Issue Date:March 2009
pp. 1-5
CMC and UMC are two prototypical instantiations of a common logical verification framework for the analysis of functional properties of service-oriented systems. The service-oriented SocL logic is used to describe the required system properties. Computatio...
     
Formal verification of an automotive scenario in service-oriented computing
Found in: Proceedings of the 13th international conference on Software engineering (ICSE '08)
By Franco Mazzanti, Maurice H. ter Beek, Nora Koch, Stefania Gnesi
Issue Date:May 2008
pp. 1-1
We report on the successful application of academic experience with formal modelling and verification techniques to an automotive scenario from the service-oriented computing domain. The aim of this industrial case study is to verify a priori, thus before ...
     
A behavioural model for product families
Found in: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering (ESEC-FSE '07)
By Alessandro Fantechi, Stefania Gnesi
Issue Date:September 2007
pp. 521-524
In this paper we propose a behavioural model, namely the Extended Modal Labeled Transition Systems, as a basis for the formalization of the different notions of variability usually present in product families definitions. In particular, an EMLTS is able to...
     
A case study on the automated verification of groupware protocols
Found in: Proceedings of the 27th international conference on Software engineering (ICSE '05)
By Alessandro Forghieri, Diego Latella, Maurice H. ter Beek, Maurizio Sebastianis, Mieke Massink, Stefania Gnesi
Issue Date:May 2005
pp. 596-603
We report on a fruitful combination of applying academic experience with formal modelling and verification techniques to an industrial case study. The goal of the case study was to investigate a priori, i.e. before implementation, the effects of adding a l...
     
Dynamic Programming as Graph Searching: An Algebraic Approach
Found in: Journal of the ACM (JACM)
By Alberto Martelli, Stefania Gnesi, Ugo Montanari
Issue Date:October 1981
pp. 737-751
It is shown that, given an arbitrary GO position on an n × n board, the problem of determining the winner is Pspace hard. New techniques are exploited to overcome the difficulties arising from the planar nature of board games. In particular, it is pro...
     
 1