Posts

"Data validation based on a formal specification of the safety requirements: 20 years of industrial experience"

  29th Brazilian Symposium on Formal Methods (SBMF 2026, https://lnkd.in/eyw_U65P ), Rio de Janeiro, 1 to 4 December. "Data validation based on a formal specification of the safety requirements: 20 years of industrial experience", by thierry lecomte , Dalay Almeida, Ph.D. and Vincent Germain, PhD ( CLEARSY ) with Michael Leuschel ( Heinrich-Heine-Universität Düsseldorf ). Two decades of academic and industrial research had to meet for this to work. On one side a rule language that separates the safety logic from the data formats. On the other a solver that grew from a research animator into an engine analysing B machines of ten million lines. Neither would have sufficed alone. And above all the work rests on human intelligence. The rules are written by engineers who understand what a system does and what it must never do. The tools check the data against those rules, they do not write them. The result is used in certified railway applications carrying nearly billions...

ABZ 2027: 13th International Conference on Rigorous State Based Methods Braga, Portugal, June 14-18, 2027

 ---------------------------------------- First Call for Papers ABZ 2027: 13th International Conference on Rigorous State Based Methods Braga, Portugal, June 14-18, 2027 https://abz-conf.org/site/2027/ ---------------------------------------- The ABZ conference is dedicated to the cross-fertilization of state-based and machine-based formal methods, like Abstract State Machines (ASM), Alloy, B, TLA, VDM and Z, that share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems. The conference aims for a vital exchange of knowledge and experience among the research communities around different formal methods. ABZ 2027 will have a main conference track, a case study track, a doctoral symposium, tutorials and workshops. ------------------- Important Dates ------------------- Abstract submission (all papers): February 8, 2027 AOE Paper submission: February 15, 2027 AOE Notificati...

Rigorous Engineering of Trustworthy Systems - Essays Dedicated to Jean-Raymond Abrial"

Egon Börger and Yamin Aït Ameur Springer LNCS 16 750  According to the latest news we collected, we expect the publication within the next month.  

A History of Formal Methods in Railways (ormal Aspects of Computing's special issue on the History of Formal Methods)

  Paper to appear in Formal Aspects of Computing's special issue on the History of Formal Methods: Maurice Ter Beek , Alessandro Fantechi, Alessio Ferrari , Stefania Gnesi , Anne Elisabeth Haxthausen , thierry lecomte : A History of Formal Methods in Railways https://lnkd.in/eeUSBTg6 Abstract. The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this paper, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modelin...

J.-R. Abrial, Foreword of the book "SPECIFICATION CASE STUDIEs" edited by Ian Hayes

 Foreword of the book "SPECIFICATION CASE STUDIEs" edited by Ian Hayes Reading formal texts is like meeting people. Sometimes, you understand them straightaway like good friends who take to each other immediately. At other times, it is more difficult. You may parse what you read, but find it impossible to work out any meaning. With the latter, you have to be patient, ask questions, explore the surroundings; in other words, it is better for you to be introduced through some common good friends who volunteer to help you prepare for the first meeting. Large computer programs, to say the least, pertain to the category of formal texts whose meanings are not immediately obvious! For that reason, people have been trying – for some time – to find out what kind of intermediate text would be best suited to play the role of go-between. This book reports on experiments made at Oxford University within this frame- work: it shows how one may communicate ideas and meanings about existing (o...

SPECIFICATION CASE STUDIES, Edited by Ian Hayes

    https://staff.itee.uq.edu.au/ianh/Papers/SCS2.pdf SPECIFICATION CASE STUDIES Second Edition Copyright c© 1987, 1992 Prentice Hall International (UK) Ltd Appendices A and B may be copied for educational purposes. Edited by Ian Hayes With Contributions by Bill Flinn Roger Gimson Steve King Carroll Morgan Ib Holm Sørensen Bernard Sufrin ii Contents I Tutorials 1 1 Small examples of specification using mathematics 3 Ian Hayes 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 A symbol table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 File update . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.4 Sorting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.5 Solutions to exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2 Block-structured symbol table 13 Ian Hayes 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Sy...

" Specification Models " Ian J. Hayes

Image