Jean-Raymond Abrial is one of the central figures in the development of formal methods for software and systems engineering. Over a career spanning more than five decades, he has played a decisive role in the creation of the Z specification notation, the B-Method, and Event-B, and in demonstrating their applicability to large-scale industrial systems. This paper presents a scholarly biographical account of Abrial's life and work, tracing the evolution of his ideas from early work on real-time languages and databases, through foundational contributions to formal specification, refinement, and proof, to the development of industrial-strength tool support such as the Atelier~B and the Rodin platform. The paper situates Abrial's contributions within their historical, intellectual, and industrial contexts, and assesses their lasting impact on software engineering and formal reasoning about programs.
翻译:让-雷蒙·阿布里亚尔是软件与系统工程形式化方法发展史上的核心人物之一。在逾五十年的职业生涯中,他在Z规范符号、B方法及Event-B的创立中发挥了决定性作用,并证明了这些方法在大型工业系统中的适用性。本文以学术传记形式梳理阿布里亚尔的生平与工作,追溯其思想从早期实时语言与数据库研究,到对形式化规范、精化及证明的基础性贡献,直至开发工业级工具支撑(如Atelier~B与Rodin平台)的演进历程。文章将阿布里亚尔的贡献置于历史、学术与工业语境中加以审视,并评估其对软件工程及程序形式化推理的持久影响。