The proceedings contain 13 papers. The topics discussed include: formal verification of steady-state errors in unity-feedback control systems; assertion-based monitoring in practice checking correctness of an automotive sensor interface; analysis of real-time properties of a digital hydraulic power management system; formal analysis of a fault-tolerant routing algorithm for a network-on-chip; formal specification and verification of TCP extended with the window scale option; learning fragments of the TCP network protocol; on the validation of an interlocking system by model-checking; deadlock avoidance in train scheduling: a model checking approach; an open alternative for SMT-based verification of SCADE models; improving static analyses of C programs with conditional predicates; detecting consistencies and inconsistencies of pattern-based functional requirements; test specification patterns for automatic generation of test sequences; and randomised testing of a microprocessor model using SMT-solver state generation.

PREFACE - Workshop on Formal Methods for Industrial Critical Systems (FMICS'14) / Flammini F; Lang F. - STAMPA. - 8718:(2014), pp. 0-0.

PREFACE - Workshop on Formal Methods for Industrial Critical Systems (FMICS'14)

Flammini F;
2014

Abstract

The proceedings contain 13 papers. The topics discussed include: formal verification of steady-state errors in unity-feedback control systems; assertion-based monitoring in practice checking correctness of an automotive sensor interface; analysis of real-time properties of a digital hydraulic power management system; formal analysis of a fault-tolerant routing algorithm for a network-on-chip; formal specification and verification of TCP extended with the window scale option; learning fragments of the TCP network protocol; on the validation of an interlocking system by model-checking; deadlock avoidance in train scheduling: a model checking approach; an open alternative for SMT-based verification of SCADE models; improving static analyses of C programs with conditional predicates; detecting consistencies and inconsistencies of pattern-based functional requirements; test specification patterns for automatic generation of test sequences; and randomised testing of a microprocessor model using SMT-solver state generation.
2014
Springer International Publishing
Geneva
Frédéric Lang, Francesco Flammini
Proceedings of the 19th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'14)
Flammini F; Lang F
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/1386630
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact