48 result(s)
Page Size: 10, 20, 50
Export: bibtex, xml, json, csv
Order by:

CNR Author operator: and / or
more
Typology operator: and / or
Language operator: and / or
Date operator: and / or
Rights operator: and / or
2021 Conference article Open Access OPEN

Spatial Model Checking for Smart Stations: Research Challenges
Ter Beek M. H., Ciancia V., Latella D., Massink M., Spagnolo G. O.
In this position paper, we discuss the introduction of spatial verification techniques in an application scenario from smart stations, viz. analysing the user experience with respect to the lighting conditions of station areas. This is a case study in industrial projects. We discuss three challenging use cases for the application of spatial model checking in this setting. First, we envision how to use the spatial model checker VoxLogicA, which can analyse both 2D and 3D voxel-based maps, to explore the areas that users can visit in a station area and to characterise them with respect to their illumination conditions. This is aimed at monitoring a smart station. We also ideate statistical spatio-temporal model checking of the design of energy-saving protocols, exploiting the modelling of user preferences. Finally, we discuss the idea of quantifying the impact of design changes, based on the logs of smart stations, to identify and measure the incidence of undesired events (e.g. non-illuminated platforms where a train is passing by) before and after each change.Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 39–47, Online conference, 24-26/08/2021
DOI: 10.1007/978-3-030-85248-1_3

See at: ISTI Repository Open Access | link.springer.com Restricted | CNR ExploRA Restricted


2020 Conference article Open Access OPEN

30 years of simulation-based quantitative analysis tools: a comparison experiment between Möbius and Uppaal SMC
Basile D., Ter Beek M. H., Di Giandomenico F., Fantechi A., Gnesi S., Spagnolo G. O.
We provide a brief comparison of the modelling and analysis capabilities of two different formalisms and their associated simulation-based tools, acquired from experimenting with these methods and tools on one specific case study. The case study is a cyber-physical system from an industrial railway project, namely a railroad switch heater, and the quantitative properties concern energy consumption and reliability. We modelled and analysed the case study with stochastic activity networks and Möbius on the one hand and with stochastic hybrid automata and Uppaal SMC on the other hand. We give an overview of the performed experiments and highlight specific features of the two methodologies. This yields some pointers for future research and improvements.Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020
DOI: 10.1007/978-3-030-61362-4_21

See at: ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | doi.org Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted


2020 Report Open Access OPEN

Specifica DOCUMENTI COMMERCIALI Secondo il provvedimento dell'Agenzia delle Entrate del 248558/2020 del 30 Giugno 2020
Spagnolo G. O., Serchiani G., Lami G.
Questo Rapporto Tecnico intende fornire una chiara e completa descrizione delle nuove operazioni del Registratore Telematico a seguito dell'emanazione da parte dell'Agenzia delle Entrate del provvedimento 248558/2020 del 30 Giugno 2020.Source: ISTI Technical Reports 2020/011, 2020, 2020
DOI: 10.32079/isti-tr-2020/011

See at: ISTI Repository Open Access | CNR ExploRA Open Access


2019 Journal article Open Access OPEN

Smart Services for Railways
Di Giandomenico F., Gnesi S, Spagnolo G. O., Fantechi A.
The project STINGRAY (SmarT station INtelliGent RAilwaY) addresses the role of the railway station, traditionally seen as a meeting point for a city, in order to enhance its importance and integration into the smart city of the future.Source: ERCIM news (2019): 34–35.

See at: ercim-news.ercim.eu Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2019 Contribution to book Open Access OPEN

QuOD: An NLP Tool to Improve the Quality of Business Process Descriptions
Ferrari A., Spagnolo G. O., Fiscella A., Parente G.
In real-world organisations, business processes (BPs) are often described by means of natural language (NL) documents. Indeed, although semi-formal graphical notations exist to model BPs, most of the legacy process knowledge--when not tacit--is still conveyed through textual procedures or operational manuals, in which the BPs are specified. This is particularly true for public administrations (PAs), in which a large variety of BPs exist (e.g., definition of tenders, front-desk support) that have to be understood and put into practice by civil servants. [Question/problem] Incorrect understanding of the BP descriptions in PAs may cause delays in the delivery of services to citizens, or, in some cases, incorrect execution of the BPs. [Principal idea/results] In this paper, we present the development of an NLP-based tool named QuOD (Quality Analyser for Official Documents), oriented to detect linguistic defects in BP descriptions and to provide recommendations for improvements. [Contribution] QuOD is the first tool that addresses the problem of identifying NL defects in BP descriptions of PAs. The tool is available online at http://narwhal.it/quod/index.html.Source: From Software Engineering to Formal Methods and Tools, and Back Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, edited by ter Beek M.H.; Fantechi A.; Semini L., pp. 267–281, 2019
DOI: 10.1007/978-3-030-30985-5_17

See at: ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | link.springer.com Restricted | link.springer.com Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted


2018 Journal article Open Access OPEN

A Guidelines framework for understandable BPMN models
Corradini F., Ferrari A., Fornari F., Gnesi S., Polini A., Re B., Spagnolo G. O.
Business process modeling allows abstracting and reasoning on how work is structured within complex organizations. Business process models represent blueprints that can serve different purposes for a variety of stakeholders. For example, business analysts can use these models to better understand how the organization works; employees playing a role in the process can use them to learn the tasks that they are supposed to perform; software analysts/developers can refer to the models to understand the system-as-is before designing the system-to-be. Given the variety of stakeholders that need to interpret these models, and considering the pivotal function that models play within organizations, understandability becomes a fundamental quality that need to be taken into particular account by modelers. In this paper we provide a set of fifty guidelines that can help modelers to improve the understandability of their models. The work focuses on the Business Process Modelling Notation 2.0 standard published by the Object Management Group, which has acquired a clear predominance among the modeling notations for business processes. Guidelines were derived by means of a thoughtful literature review - which allowed identifying around one hundred guidelines - and through successive activities of synthesis and homogenization. In addition, we implemented a freely available open source tool, named BEBoP (understandaBility vErifier for Business Process models), to check the adherence of a model to the guidelines. Finally, guidelines violation has been checked with BEBoP on a dataset of 11,294 models available in a publicly accessible repository. Our tests show that, although the majority of the guidelines are respected by the models, some guidelines, which are recognized as fundamental by the literature, are frequently violated.Source: Data & knowledge engineering 113 (2018): 129–154. doi:10.1016/j.datak.2017.11.003
DOI: 10.1016/j.datak.2017.11.003
Project(s): LEARN PAD via OpenAIRE

See at: ISTI Repository Open Access | Data & Knowledge Engineering Restricted | Data & Knowledge Engineering Restricted | Data & Knowledge Engineering Restricted | Data & Knowledge Engineering Restricted | Data & Knowledge Engineering Restricted | Data & Knowledge Engineering Restricted | Data & Knowledge Engineering Restricted | CNR ExploRA Restricted | Data & Knowledge Engineering Restricted | www.sciencedirect.com Restricted


2018 Journal article Open Access OPEN

Improving the quality of business process descriptions of public administrations: resources and research challenges
Ferrari A., Witschel H. F., Spagnolo G. O., Gnesi S.
Purpose Business processes of public administrations (PAs) are often described in the form of written procedures or operational manuals. These busi- ness process descriptions are expected to be properly understood and applied by civil servants, who have to provide legally-compliant service provisions to the citizens. However, process descriptions in the PA are sometimes hard to read, ambiguous, or vague, leading to false interpretations or even incorrect execu- tion of the processes. In this paper, we focus on improving the descriptions of business processes to be used in PAs. Design/methodology/approach To this end, we present an in-depth domain analysis, including a literature review and interviews with PA stakeholders belonging to different realities. From this analysis, we identified a set of 52 typical defects of process descriptions. Findings We provide a set of guidelines and a template to constrain the definition of these documents and to mitigate the identified defects. Furthermore, we outline research challenges in the field of quality assessment of textual process descriptions for the PA. Research limitations/implications This paper addresses the needs of any PA officer who has to write an official procedure or operational manual, and should be studied by researchers who wish to provide automatic strategies to check the quality of these documents. Originality/value Text quality issues have been addressed in various fields (e.g., requirements engineering), but not in the area of business process descriptions of PAs. Our contribution consists in the study of the quality issues that occur and create problems in the practice of this particular domain. Based on this insight, we provide directions for research that will find solutions to mitigate the issues.Source: Business process management journal 24 (2018): 49–66. doi:10.1108/BPMJ-05-2016-0096
DOI: 10.1108/bpmj-05-2016-0096
Project(s): LEARN PAD via OpenAIRE

See at: ISTI Repository Open Access | Business Process Management Journal Open Access | Business Process Management Journal Restricted | Business Process Management Journal Restricted | Business Process Management Journal Restricted | Business Process Management Journal Restricted | CNR ExploRA Restricted | Business Process Management Journal Restricted | Business Process Management Journal Restricted


2018 Journal article Open Access OPEN

Towards formal methods diversity in railways: an experience report with seven frameworks
Mazzanti F., Ferrari A., Spagnolo G. O.
In the ever expanding universe of formal methods, several tools exist that can be exploited to validate early system designs, and that are applicable to problems of the railway domain. In this paper, we present an experience report in formal modelling and verification using seven different formal environments, namely UMC, Promela/SPIN, NuSMV, mCRL2, CPN Tools, FDR4 and CADP. In particular, we model and verify an algorithm that addresses a typical railway problem, namely deadlock avoidance in train scheduling. The algorithm is designed according to a prototypical architecture, the so-called blackboard pattern, in which a set of global data are atomically updated by a set of concurrent guarded agents. Our experience, limited to the specific problem, shows that the design of the algorithm can be translated into the different formalisms with acceptable effort, while deep proficiency with the tools is required to optimise the performance. The current paper establishes the preliminary foundations for the concept of formal methods diversity in the development of railway systems. The concept is based on the idea that if different non-certified formal environments are used to verify the same design, this increases the confidence on the verification results. Furthermore, by checking that the number of states generated during the verification process is the same for each framework, the designer can have an initial indication of the equivalence of the diverse models. The industrial application of this promising concept requires further research, and appropriate guidelines shall be established to identify the proper formal environments to use for a specific railway problem, and to define an industrial process in which formal methods diversity can be exploited at its full benefits. The paper presents the different models developed, compares the tools employed in terms of language features and performance, and discusses the industrial implications of the concept of formal methods diversity in the railway domain.Source: International journal on software tools for technology transfer (Print) 20 (2018): 263–288. doi:10.1007/s10009-018-0488-3
DOI: 10.1007/s10009-018-0488-3
Project(s): ASTRail via OpenAIRE

See at: ISTI Repository Open Access | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | CNR ExploRA Restricted


2017 Report Closed Access

Registratori telematici: modello di processo per l'approvazione degli apparecchi misuratori fiscali
Spagnolo G. O., Serchiani G., Lami G.
Present the business process model of the certification of Registratori Telematici to italian fiscal market.Source: ISTI Technical reports, 2017

See at: CNR ExploRA Restricted


2017 Report Open Access OPEN

Quality assessment strategy: applying business process understandability guidelines for learning
Corradini F., Ferrari A., Fornari F., Gnesi S., Polini A., Re B., Spagnolo G. O.
Modelling using graphical notations permits to improve communications among stakeholders. The usage and composition of the notation elements can greatly impact on the understandability of the dened models. This is an important factor to consider in complex organizations where activities are performed by the collaboration of many stakeholders. Understandability becomes even more important when models are also used to structure learning activities. In this technical we report our experience on the usage of BPMN for documenting and learning business process activities.Source: ISTI Technical reports, 2017
Project(s): LEARN PAD via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Open Access


2017 Conference article Restricted

Towards the automation of the travel management procedure of an italian public administration
Calabro A., Marchetti E., Spagnolo G. O., Cempini P., Mancini L., Paoletti S.
Recently the Public Administrations pay a lot of attention to decreases the time required for document production and validation specifically in case of travel management. In this paper we describe the procedural steps followed to implement a first prototype framework for automating the travel management process adopted inside an Italian PA. To achieve this goal, we represent the process through Business Models specified into a formal notations. The experience highlighted important challenges in the application of automatic facilities for the travel management and let the detection of inconsistencies and improvements of the process itself.Source: Software Quality. 9th International Conference on Complexity and Challenges of Software Engineering in Emerging Technologies, pp. 175–187, Vienna, Austria, 17-20 January 2017
DOI: 10.1007/978-3-319-49421-0_12

See at: academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | link.springer.com Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted


2017 Conference article Restricted

Checking business process modeling guidelines in apromore
Fornari F., Gnesi S., La Rosa M., Polini A., Re B., Spagnolo G. O.
We present the integration of BEBoP - understandaBility vErifier for Business Process models, into the Apromore open-source process analytics platform. Given a BPMN model the tool allows one to verify which understandability modeling guidelines such as layout conventions are violated by the model. Such guidelines are rules that a model designer should follow to guarantee that the designed model is easy to understand by relevant stakeholders. Given the variety of stakeholders that need to interpret these models, and considering the pivotal function that process models play within organizations, understandability becomes a fundamental quality requirement that needs to be taken into account by designers. The tool provides model designers with textual and graphical representations of which understandaiblity guidelines are violated. Designers can then decide to repair models in such a way to guarantee a higher degree of understandability.Source: BPM Demo Track and BPM Dissertation Award, Barcellona, 13/09/2017

See at: ceur-ws.org Restricted | CNR ExploRA Restricted


2017 Conference article Restricted

Towards a dataset for natural language requirements processing
Ferrari A., Spagnolo G. O., Gnesi S.
[Context and motivation] The current breakthrough of natural language processing (NLP) techniques can provide the requirements engineering (RE) community with powerful tools that can help addressing specic tasks of natural language (NL) requirements analysis, such as traceability, ambiguity detection and requirements classification, to name a few. [Question/problem] However, modern NLP techniques are mainly statistical, and need large NL requirements datasets, to support appropriate training, test and validation of the techniques. The RE community has experimented with NLP since long time, but datasets were often proprietary, or limited to few software projects for which requirements were publicly available. Hence, replication of the experiments and generalization have always been an issue. [Principal idea/results] Our near future commitment is to provide a publicly available NL requirements dataset. [Contribution] To this end, we are collecting requirements documents from the Web, and we are representing them in a common XML format. In this paper, we present the current version of the dataset, together with our agenda concerning formatting, extension, and annotation of the dataset.Source: joint REFSQ Workshops, Doctoral Symposium, Research Method Track, and Poster Track, 27/02/2017

See at: ceur-ws.org Restricted | CNR ExploRA Restricted


2017 Conference article Restricted

PURE: A Dataset of Public Requirements Documents
Ferrari A., Spagnolo G. O., Gnesi S.
This paper presents PURE (PUblic REquirements dataset), a dataset of 79 publicly available natural language requirements documents collected from the Web. The dataset includes 34,268 sentences and can be used for natural language processing tasks that are typical in requirements engineering, such as model synthesis, abstraction identification and document structure assessment. It can be further annotated to work as a benchmark for other tasks, such as ambiguity detection, requirements categorisation and identification of equivalent re-quirements. In the paper, we present the dataset and we compare its language with generic English texts, showing the peculiarities of the requirements jargon, made of a restricted vocabulary of domain-specific acronyms and words, and long sentences. We also present the common XML format to which we have manually ported a subset of the documents, with the goal of facilitating replication of NLP experiments.Source: 25th IEEE International Requirements Engineering Conference, pp. 502–505, Lisbon, Portugal, 04/09/2017
DOI: 10.1109/re.2017.29

See at: academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | ieeexplore.ieee.org Restricted | ieeexplore.ieee.org Restricted | CNR ExploRA Restricted | xplorestaging.ieee.org Restricted


2017 Journal article Open Access OPEN

The KandIStI/UMC Online Open-Access Verification Framework
Mazzanti F., Ferrari A., Spagnolo G. O.
ISTI-CNR provides an online open-access environment for the experimentation of design, analysis and verification of UML-based system models. Great as a didactic environment, it can successfully compete in terms of friendliness and usability with the most mainstream verification frameworks.Source: ERCIM news (2017): 56–57.

See at: ercim-news.ercim.eu Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2017 Journal article Open Access OPEN

Avoiding Gridlocks in the Centralised Dispatching of a Fleet of Autonomous Vehicles
Mazzanti F., Ferrari A., Spagnolo G. O.
Autonomous vehicles will become pervasive in the near future. The TRACE-IT project is investigating how gridlocks may be avoided.Source: ERCIM news (2017): 42–42.

See at: ercim-news.ercim.eu Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2017 Conference article Open Access OPEN

Improving a Travel Management Procedure: an Italian Experience
Calabro A., Marchetti E., Spagnolo G. O., Cempini P., Mancini L., Paoletti S.
Recently, a lot of attention has been dedicated by the Public Administrations to reduce/optimize the costs of travel management. Indeed, automatic support may increase the quality of the proposed services, drastically decreasing the time required for document production and validation, and promoting the integration with different PA (Public Administration) systems and services. However, due to the critical nature of the exchanged data, the interaction with the customers (personnel and citizens), the complexity of the considered procedures, the quality aspect becomes a crucial point to be considered during the development of automatic supports. In this paper, we focus on the quality aspects of the PA travel management automation, and we present the evaluation of a prototype implementation of a framework for automating the travel management process adopted inside an Italian PA. The experience highlighted important challenges in the application of automatic facilities for the travel management and nd allowed the detection of inconsistencies and improvements of the process itself.Source: SOFTENG 2017 - Third International Conference on Advances and Trends in Software Engineering, pp. 114–119, Venice, Italy, 23-27 April 2017

See at: CNR ExploRA Open Access | www.iaria.org Open Access


2017 Contribution to conference Open Access OPEN

Deadlock free dispatching for fleets of vehicles
Mazzanti F., Ferrari A., Spagnolo G. O.
Formalizzazione e verifica di un algorithmo di dispatching deadlock free.Source: Forum Méthodes Formelles - "Véhicules Autonomes et Méthodes Formelles", Toulouse FRANCE, 10/10/2017
Project(s): ASTRail via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Open Access | zenodo.org Open Access


2016 Conference article Restricted

An experience on applying process mining techniques to the tuscan port community system
Spagnolo G. O., Marchetti E., Coco A., Scarpellini P., Querci A., Fabbrini F., Gnesi S.
[Context & Motivation] The Business Process Management is an important and widespread adopted proposal for modelling process specifications and developing an executable framework for the management of the process itself. In particular the monitoring facilities associated to the on-line process execution provide an important means to the control of process evolution and quality. In this context, this paper provides an experience on the application of business process modelling techniques and process mining techniques to the TPCS, Tuscan Port Community System. This is a web-services based platform with multilevel access control and data recovery facilities, developed for supporting and strengthening the Motorways of the Sea and Italian regulations. The paper describes a storytelling approach applied to derive the TPCS business process model and the conformance checking techniques used to validate it and improve the overall TPCS software quality.Source: Software Quality. The Future of Systems and Software Development. 8th International Conference, pp. 49–60, Vienna, Austria, 18-21/01/2016
DOI: 10.1007/978-3-319-27033-3_4

See at: academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | link.springer.com Restricted | link.springer.com Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted | rd.springer.com Restricted


2016 Software Unknown

Verification component understandability BPMN
Spagnolo G. O., Ferrari A.
In Learn PAd, we developed a quality assessment strategy that allows to guarantee that the used BP models result being understandable by the civil servants. The quality assessment strategy includes modeling understandability guidelines which are supported by a Java tool called verification component understandability BPMN.Project(s): LEARN PAD via OpenAIRE

See at: github.com | CNR ExploRA