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.I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.