现代技术系统大多依赖于复杂控制技术、计算机技术和网络通信技术。由于各种信号并发、冲突等的存在,导致系统的动态行为错综复杂。因此,往往将这些系统抽象为离散事件控制系统来研究。动态可重构系统是未来复杂技术系统的趋势,如安全关键的核电系统、飞控系统和普通的汽车电子系统、自动化制造系统等。这种系统可以根据系统内、外执行环境的变化,如部分组件故障、网络阻塞、未知干扰、用户请求等,主动地修改当前构型的部分组件、组件间连接关系和数据等,使当前构型在线地转变为另一种构型,从而保证系统能够持续地满足控制需求。基于模型的设计方法能够较早发现复杂技术系统的设计缺陷、提高系统的可靠性、缩短开发系统所耗费的时间,因此被广泛地关注和应用。一个准确、简洁且易于分析的系统形式化模型是基于模型设计方法的第一步。在此基础上采用形式化验证方法能够全面测试被设计的系统是否满足需求并为改进系统设计方案提供可靠依据。本文研究的主要内容就是可重构离散事件控制系统的形式化建模与验证。NCES是Petri网的一种模块化扩展形式化体系。其清晰的模块化结构适合于建模可重构离散事件控制系统。本文首先重点研究了三种基于NCES网的可能的重构方案：第一种是对库所的修改,第二种是对变迁的修改,第三种是对系统初始标识的修改。相应地,一种基于NCES的嵌套的状态机被用来分别处理这三种重构方案的控制实施。最终得到的系统模型的正确性由软件SESA检验,其中功能特性由计算树逻辑及其扩展逻辑描述。考虑到直接用NCES或者TNCES建模可重构控制系统会给后续系统验证带来较大负担,本文提出了一种新的形式化体系R-TNCES。一个R-TNCES由一个控制模块和一个行为模块组成。其中,行为模块由多个交叠的TNCES组成,控制模块由一组重构函数组成。这些重构函数根据执行环境的改变自动地切换行为模块中的TNCES.此外,考虑到R-TNCES中各个TNCES的相似性,一个分层验证的方法被提了出来,用以控制对R-TNCES验证的复杂性。为了保证分布式可重构离散事件控制系统的一致性,本文提出了一种新的协调方法。系统中的每一个可重构的分系统都由一个R-TNCES来表示。一个虚拟协调器和该协调器与各分系统间的通信协议被建立起来处理分系统间的一致性问题。这种方法可以达到两个效果：1)给出最优重构方案,2)减少分系统间的通信量。此外,为了保证这种协调方法的正确性,采用了基于计算树逻辑的模型检验技术来验证整个系统的各种行为。最后,为了有效分析动态重构过程中的系统行为,本文进一步扩展了R-TNCES。首先,在重构函数中附加了作用范围和并发决策函数。其次,对事件发射规则做了修改,使得重构事件和普通事件能够有条件地并发。同样地,为了保证系统的正确性,本文借助于软件SESA完成对扩展的R-TNCES的形式化验证。一个可重构、节能的汽车装配系统被用来说明这一部分工作的优点和有效性。