Alessandro Fantechi

Proceedings of the Model-Driven Engineering and Software Development, 2016

Petri Nets Modeling for the Schedulability Analysis of Industrial Real Time Systems.

[BibT_eX]

[DOI]

Stefano Pepi

Proceedings of the International Workshop on domAin specific Model-based AppRoaches to vErificaTion and validaTiOn, 2016

Compositional Verification of Multi-station Interlocking Systems.

[BibT_eX]

[DOI]

Hugo Daniel Macedo

Anne E. Haxthausen

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Formal Methods and Safety Certification: Challenges in the Railways Domain.

[BibT_eX]

[DOI]

Alessio Ferrari

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Variability-Based Design of Services for Smart Transportation Systems.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Formal Techniques for a Data-Driven Certification of Advanced Railway Signalling Systems.

[BibT_eX]

[DOI]

Proceedings of the Critical Systems: Formal Methods and Automated Verification, 2016

Refinement of Behavioural Models for Variability Description.

[BibT_eX]

[DOI]

Proceedings of the From Action Systems to Distributed Systems - The Refinement Approach., 2016

2015

Using FMC for family-based analysis of software product lines.

[BibT_eX]

[DOI]

Proceedings of the 19th International Conference on Software Product Line, 2015

Applying the product lines paradigm to the quantitative analysis of collective adaptive systems.

[BibT_eX]

[DOI]

Maurice H. ter Beek

Proceedings of the 19th International Conference on Software Product Line, 2015

2014

Formal methods for railway control systems.

[BibT_eX]

[DOI]

Francesco Flammini

Int. J. Softw. Tools Technol. Transf., 2014

Validation of Interlocking Systems by Testing their Models.

[BibT_eX]

[DOI]

Andrea Bonacchi

Proceedings of the 9th International Conference on the Quality of Information and Communications Technology, 2014

Model-based development of an automatic train operation component for communication based train control.

[BibT_eX]

[DOI]

Proceedings of the 17th International IEEE Conference on Intelligent Transportation Systems, 2014

Challenges in Modelling and Analyzing Quantitative Aspects of Bike-Sharing Systems.

[BibT_eX]

[DOI]

Maurice H. ter Beek

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, 2014

On the Validation of an Interlocking System by Model-Checking.

[BibT_eX]

[DOI]

Andrea Bonacchi

Proceedings of the Formal Methods for Industrial Critical Systems, 2014

2013

Using Temporal Logic and Model Checking in Automated Recognition of Human Activities for Ambient-Assisted Living.

[BibT_eX]

[DOI]

IEEE Trans. Hum. Mach. Syst., 2013

Model-Based Development and Formal Methods in the Railway Industry.

[BibT_eX]

[DOI]

IEEE Softw., 2013

The Metrô Rio case study.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2013

Session types for safe Web service orchestration.

[BibT_eX]

[DOI]

Jonathan Michaux

J. Log. Algebraic Methods Program., 2013

An On-line system for automated recognition of human activities.

[BibT_eX]

[DOI]

Eur. J. Law Technol., 2013

SYRMA: a tool for a system approach to risk management in mission critical systems.

[BibT_eX]

[DOI]

Int. J. Bus. Inf. Syst., 2013

Safe Session-Based Service Orchestration with Unreliable Communication.

[BibT_eX]

[DOI]

Jonathan Michaux

Proceedings of the Web Services and Formal Methods - 10th International Workshop, 2013

Topologically configurable systems as product families.

[BibT_eX]

[DOI]

Proceedings of the 17th International Software Product Line Conference, 2013

Stochastic Model-Based Analysis of Railway Operation to Support Traffic Planning.

[BibT_eX]

[DOI]

Felicita Di Giandomenico

Massimiliano Leone Itria

Proceedings of the Software Engineering for Resilient Systems, 5th International Workshop, 2013

Twenty-Five Years of Formal Methods and Railways: What Next?

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods, 2013

Validation of Railway Interlocking Systems by Formal Verification, A Case Study.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods, 2013

Resource-oriented design towards the convergence of Web-centric and Telecom-centric services.

[BibT_eX]

[DOI]

Proceedings of the Second International Conference on Future Generation Communication Technologies (FGCT 2013), 2013

2012

A logical verification methodology for service-oriented computing.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2012

Adding Sessions to BPEL

[BibT_eX]

[DOI]

Jonathan Michaux

Proceedings of the Proceedings 8th International Workshop on Automated Specification and Verification of Web Systems, 2012

A GUI Testability Problem: A Case Study in the Railway Signaling Domain.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on the Quality of Information and Communications Technology, 2012

Lessons Learnt from the Adoption of Formal Model-Based Development.

[BibT_eX]

[DOI]

Alessio Ferrari

Proceedings of the NASA Formal Methods, 2012

Formal Methods for Intelligent Transportation Systems.

[BibT_eX]

[DOI]

Francesco Flammini

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, 2012

Distributing the Challenge of Model Checking Interlocking Control Tables.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, 2012

A Compositional Framework to Derive Product Line Behavioural Descriptions.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, 2012

2011

Preface to the special issue on Formal Methods for Industrial Critical Systems (FMICS 2007 + FMICS 2008).

[BibT_eX]

[DOI]

Sci. Comput. Program., 2011

A state/event-based model-checking approach for the analysis of abstract system properties.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2011

Adoption of Model-Based Testing and Abstract Interpretation by a Railway Signalling Manufacturer.

[BibT_eX]

[DOI]

Int. J. Embed. Real Time Commun. Syst., 2011

Formal Description of Variability in Product Families.

[BibT_eX]

[DOI]

Proceedings of the Software Product Lines - 15th International Conference, 2011

Variability and Rigour in Service Computing Engineering.

[BibT_eX]

[DOI]

Proceedings of the 34th Annual IEEE Software Engineering Workshop, 2011

On the Adoption of Model Checking in Safety-Related Software Industry.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2011

Design and validation of variability in product lines.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Product Line Approaches in Software Engineering, 2011

A Model-Checking Tool for Families of Services.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2011

2010

A Deontic Logical Framework for Modelling Product Families.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Workshop on Variability Modelling of Software-Intensive Systems, 2010

An industrial application of formal model based development: the Metrô Rio ATP case.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Software Engineering for Resilient Systems, 2010

An experience in using a tool for evaluating a large set of natural language requirements.

[BibT_eX]

[DOI]

Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), 2010

A Logical Framework to Deal with Variability.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 8th International Conference, 2010

Model Based Testing and Abstract Interpretation in the Railway Signaling Context.

[BibT_eX]

[DOI]

Proceedings of the Third International Conference on Software Testing, 2010

Model Checking Interlocking Control Tables.

[BibT_eX]

[DOI]

Proceedings of the FORMS/FORMAT 2010, 2010

The Metrô Rio ATP Case Study.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2010

Modeling Variability, Evolvability, and Adaptability in Service Computing (a vision for future research).

[BibT_eX]

[DOI]

Proceedings of the 1st International Workshop on Automated Configuration and Tailoring of Applications, 2010

2009

Deontic Logics for Modeling Behavioural Variability.

[BibT_eX]

[DOI]

Proceedings of the Third International Workshop on Variability Modelling of Software-Intensive Systems, 2009

Modeling Guidelines for Code Generation in the Railway Signaling Context.

[BibT_eX]

Proceedings of the First NASA Formal Methods Symposium, 2009

Formal Development for Railway Signaling Using Commercial Tools.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2009

2008

Experimenting with Diversity in the Formal Development of Railway Signalling Systems.

[BibT_eX]

[DOI]

Giovanni Lombardi

ERCIM News, 2008

Evaluation of Natural Language Requirements in the MODCONTROL Project.

[BibT_eX]

[DOI]

ERCIM News, 2008

Model driven development of railway systems using diversity.

[BibT_eX]

Comput. Syst. Sci. Eng., 2008

Formal Modeling for Product Families Engineering.

[BibT_eX]

[DOI]

Proceedings of the Software Product Lines, 12th International Conference, 2008

QuARS Express - A Tool Demonstration.

[BibT_eX]

[DOI]

Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 2008

SensoriaPatterns: Augmenting Service Engineering with Formal Analysis, Transformation and Dynamicity.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, 2008

Panel Discussion on Formal Methods in Commercial Software Development Tools.

[BibT_eX]

[DOI]

Alessio Ferrari

Proceedings of the Formal Methods for Industrial Critical Systems, 2008

A Model Checking Approach for Verifying COWS Specifications.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2008

Session Types for Orchestration Charts.

[BibT_eX]

[DOI]

Proceedings of the Coordination Models and Languages, 10th International Conference, 2008

2007

A behavioural model for product families.

[BibT_eX]

[DOI]

Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007

Experimenting with diversity in the model driven development of a railway signaling system.

[BibT_eX]

[DOI]

Proceedings of the 2007 Workshop on Engineering Fault Tolerant Systems, 2007

Model Driven Development and Code Generation: An Automotive Case Study.

[BibT_eX]

[DOI]

Proceedings of the SDL 2007: Design for Dependable Systems, 2007

An Action/State-Based Model-Checking Approach for the Analysis of Communication Protocols for Service-Oriented Applications.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2007

2006

Statecharts Composition to Model Topologically Distributed Applications.

[BibT_eX]

[DOI]

Michele Banci

Trans. SDPS, 2006

Product Line Use Cases: Scenario-Based Specification and Testing of Requirements.

[BibT_eX]

[DOI]

Proceedings of the Software Product Lines - Research Issues in Engineering and Management, 2006

Achieving Fault Tolerance by a Formally Validated Interaction Policy.

[BibT_eX]

[DOI]

Laura Semini

Proceedings of the Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project], 2006

A Story About Formal Methods Adoption by a Railway Signaling Manufacturer.

[BibT_eX]

[DOI]

Proceedings of the FM 2006: Formal Methods, 2006

2005

A comparison between handwritten and automatic generation of C code from SDL using static analysis.

[BibT_eX]

[DOI]

Softw. Pract. Exp., 2005

Assembling components with behavioural contracts.

[BibT_eX]

[DOI]

Cyril Carrez

Ann. des Télécommunications, 2005

A Content Analysis Technique for Inconsistency Detection in Software Requirements Documents.

[BibT_eX]

[DOI]

Emilio Spinicci

Proceedings of the Anais do WER05, 2005

Instantiating generic charts for railway interlocking systems.

[BibT_eX]

[DOI]

Michele Banci

Proceedings of the 10th international workshop on Formal methods for industrial critical systems, 2005

2004

Enhancing Test Coverage by Back-tracing Model-checker Counterexamples.

[BibT_eX]

[DOI]

Adriana Maggiore

Proceedings of the International Workshop on Test and Analysis of Component Based Systems, 2004

Geographical Versus Functional Modelling by Statecharts of Interlocking Systems.

[BibT_eX]

[DOI]

Michele Banci

Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems, 2004

Validation Coverage for a Component-based SDL model of a Railway Signaling System.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Test and Analysis of Component Based Systems, 2004

A Methodology for the Derivation and Verification of Use Cases for Product Lines.

[BibT_eX]

[DOI]

Proceedings of the Software Product Lines, Third International Conference, 2004

Witness and Counterexample Automata for ACTL.

[BibT_eX]

[DOI]

Robert Meolic

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2004

Natural Language Processing of Patents and Technical Documentation.

[BibT_eX]

[DOI]

Gaetano Cascini

Emilio Spinicci

Proceedings of the Document Analysis Systems VI, 6th International Workshop, 2004

2003

Applications of linguistic techniques for use case analysis.

[BibT_eX]

[DOI]

Requir. Eng., 2003

Modelling and Validating a multiple-configuration railway signalling system using SDL.

[BibT_eX]

[DOI]

Emilio Spinicci

Proceedings of the International Workshop on Test and Analysis of Component-Based Systems, 2003

Elicitation of Use Cases for Product Lines.

[BibT_eX]

[DOI]

Proceedings of the Software Product-Family Engineering, 5th International Workshop, 2003

Behavioural Contracts for a Sound Assembly of Components.

[BibT_eX]

[DOI]

Cyril Carrez

Proceedings of the Formal Techniques for Networked and Distributed Systems - FORTE 2003, 23rd IFIP WG 6.1 International Conference, Berlin, Germany, September 29, 2003

2002

Model checking fault tolerant systems.

[BibT_eX]

[DOI]

Softw. Test. Verification Reliab., 2002

Application of Linguistic Techniques for Use Case Analysis.

[BibT_eX]

[DOI]

Proceedings of the 10th Anniversary IEEE Joint International Conference on Requirements Engineering (RE 2002), 2002

2001

Formal validation of fault-tolerance mechanisms inside GUARDS.

[BibT_eX]

[DOI]

Reliab. Eng. Syst. Saf., 2001

Design Validation of Embedded Dependable Systems.

[BibT_eX]

[DOI]

IEEE Micro, 2001

Finite Approximations for Model Checking Non-finite-state Processes.

[BibT_eX]

[DOI]

Nicoletta De Francesco

Paola Inverardi

Comput. J., 2001

2000

Formally Verifying Fault Tolerant System Designs.

[BibT_eX]

[DOI]

Luca Simoncini

Comput. J., 2000

1999

GUARDS: A Generic Upgradable Architecture for Real-Time Dependable Systems.

[BibT_eX]

[DOI]

IEEE Trans. Parallel Distributed Syst., 1999

Formal Validation of the GUARDS Inter-Consistency Mechanism.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 1999

1998

A Formal Verification Environment for Railway Signaling System Design.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1998

Validating the Design of Dependable Systems.

[BibT_eX]

[DOI]

Luca Simoncini

Proceedings of the 1st International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC '98), 1998

A Symbolic Model Checker for ACTL.

[BibT_eX]

[DOI]

Proceedings of the Applied Formal Methods, 1998

1997

An industrial application for the JACK environment.

[BibT_eX]

[DOI]

J. Syst. Softw., 1997

Object-Oriented Analysis of COBOL.

[BibT_eX]

[DOI]

Paolo Nesi

E. Somma

Proceedings of the 1st Euromicro Working Conference on Software Maintenance and Reengineering (CSMR '97), 1997

1996

Formal Verification of Safety Requirements on Complex Systems.

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Computer Safety, 1996

Proving Safety Properties for Embedded Control Systems.

[BibT_eX]

[DOI]

Proceedings of the Dependable Computing, 1996

Towards Automatic Temporal Logic Verification of Value Passing Process Algebra Using Abstract Interpretation.

[BibT_eX]

[DOI]

Diego Latella

Proceedings of the CONCUR '96, 1996

1995

Model Checking of Non-Finite State Processes by Finite Approximations.

[BibT_eX]

[DOI]

Nicoletta De Francesco

Paola Inverardi

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1995

Application of Correctness Preserving Transformations for Deriving Architectural Descriptions of Interactive Systems from User Interface Specifications.

[BibT_eX]

Fabio Paternò

Proceedings of the SEKE'95, 1995

An Experience in Formal Verification of Safety Properties of a Railway Signalling Control System.

[BibT_eX]

[DOI]

Proceedings of the 14th International Conference on Computer Safety, 1995

Verifying hardware components within JACK.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1995

1994

Assisting Requirement Formalization by Means of Natural Language Translation.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1994

Model Checking for Action-Based Logics.

[BibT_eX]

[DOI]

Gioia Ristori

Formal Methods Syst. Des., 1994

Tableau methods to describe strong bisimilarity on LOTOS processes involving pure interleaving and enabling.

[BibT_eX]

R. Sacchelli

Proceedings of the Formal Description Techniques VII, 1994

Formal Reasoning on Fault Coverage of Fault Tolerant Techniques: A Case Study.

[BibT_eX]

[DOI]

Luca Simoncini

Proceedings of the Dependable Computing, 1994

1993

An Action-Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems.

[BibT_eX]

[DOI]

Comput. Networks ISDN Syst., 1993

An Expressive Logic for Basic Process Algebra.

[BibT_eX]

[DOI]

V. Perticaroli

Proceedings of the Mathematical Foundations of Computer Science 1993, 1993

1991

Executing the formal definition of Ada.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 1991

Compositionality and Bisimulation: A Negative Result.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1991

1990

Compositional logic semantics and LOTOS.

[BibT_eX]

Gioia Ristori

Proceedings of the Protocol Specification, 1990

How Expressive Are LOTOS Behaviour Expressions?

[BibT_eX]

Gianluca Mazzarini

Proceedings of the Formal Description Techniques, 1990

1989

An Expressive Temporal Logic for Basic LOTOS.

[BibT_eX]

Cosimo Laneve

Proceedings of the Formal Description Techniques, 1989

1987

Distributed Implementation of Nested Communicating Sequential Processes: Communication and Termination.

[BibT_eX]

[DOI]

J. Parallel Distributed Comput., 1987

An Executon Environment for the Formal Definiton of Ada.

[BibT_eX]

[DOI]

Proceedings of the ESEC '87, 1987

1986

Using High Level Languages for Local Computer Network Communication: A Case Study in Ada.

[BibT_eX]

Paola Inverardi

Norma Lijtmaer

Softw. Pract. Exp., 1986

Testing Equivalences for Event Structures.

[BibT_eX]

[DOI]

Luca Aceto

Rocco De Nicola

Proceedings of the Mathematical Models for the Semantics of Parallelism, Advanced School, Rome, Italy, September 24, 1986

1982

Portable Ada programming system: a proposed run-time architecture.

[BibT_eX]

[DOI]