自动化生产线是现代产品生产过程中一种控制系统,具有工作效率高,加工质量好,生产成本低的特点。自动化生产线通常由各种机械和电控设备组成,功能可以几乎包含了生产工艺的各个环节,使得它具有较高集成度,并且具有较高的自动化水平,可以有效减少人工操作,这些特点决定了设计的自动化生产线应具有较高的可靠性。在生产线正式投入工作前,要经过长期、大量的测试,用来发现程序中的错误,验证控制程序的正确性。但在实际情况中,有些错误可能由于测试时间和方法的不足,并没有通过测试检测出来;还有一些错误状况,由于现场条件的限制,无法制造条件进行测试。为了解决这一类问题,形式化方法应运而生。形式化方法通过数学的方法,对实际系统进行数学建模和验证,可以在不经过测试的条件下对系统进行验证,提高系统的可靠性,有效地降低了测试成本,适用于对可靠性要求高的场合。本文的内容是125I自动化生产线设计和可靠性验证,主要包括对生产线的结构、功能及相关控制技术的介绍,并且详细说明了PLC控制系统的设计方法。除此之外,由于125I生产线用于生产放射性药物,对控制程序有着较高的可靠性要求。因此,除了对生产线控制程序进行了常规的仿真和测试外,还对所设计的控制程序探究性地进行了Event-B形式化建模和验证,并介绍了相关的形式化方法原理,详细说明了Event-B方法的建模和验证过程。