Formal methods and hybrid real time systems

Více o knize

This collection explores various aspects of formal methods and system modeling, focusing on applications in areas such as distributed file replication, traffic systems, and embedded systems. It delves into denotational semantics for programming languages like Handel-C and discusses generating polynomial invariants using tools like DISCOVERER and QEPCAD. The text highlights the CoCoME experience in harnessing rCOS for tool support and automating verification processes in cooperative and control systems. It also covers specifying time models with temporal propositional variables in Duration Calculus and the importance of ordering connections to relate domain concepts intensionally. The work emphasizes the significance of formal methods in industrial contexts, proving theorems about JML classes, and developing specifications for testing. It presents a model-based approach for constructing and verifying railway control systems, addresses compensable programs, and discusses the engineering of embedded systems. The collection also features design verification patterns, the revival of Algol concepts in modern programming, and symbolic test generation using temporal logic. It concludes with a formal approach to railway applications and the paradigm of services as a computation model, showcasing the breadth and depth of formal methods in contemporary software engineering.