随着硬件技术进步和软件技术积累,软件复杂度随着软件体量日益增加。如何保证软件可靠性越来越得到人们重视。采用基于模型的形式化方法对软件建模以及模型的正确性验证是当前行之有效的方法。本课题针对软件开发的不同阶段,使用形式化建模方法的方法保证需求的正确性。在软件完成后,使用自适应随机测试方法保证程序的正确性。状态变迁矩阵(STM)形式化建模方法能应用在软件开发的各个阶段。针对STM中单元格处理对多变量嵌套判断问题上不完善,提出引入决策表的STM形式化建模方法。通过建模过程中确认需求多个变量关系以及变量的划分区间,完整填入决策表中。使用C4.5决策树生成算法生成,能生成条件判断最少的分支结构。在决策树中引入权重,能使决定不同属性判断的先后顺序,生成更符合实际情况的分支,更具逻辑性。最后通过程序代码转化算法,生成具有编码规范的程序代码,使代码更易理解,降低日后修订查阅的成本。最后通过分层建模实例以及生成的程序代码,说明建模方法的可操作与正确性。对于STM正确性的验证问题,针对已有的验证方法不足,提出黑盒测试的STM的自适应测试方法,该方法测试成本低,并在一定程度上弥补其余方法的不足。方法采用FSCS算法,并对其变量距离计算进行改进,通过每次选取已生成与已测用例距离最远的测试用例来作为下一个测试用例。STM中随机事件序列生成与测试用例的距离衡量是研究的重点。通过将事件序列与输入变量联合生成测试路径,将测试路径距离转换为字符串之间的编辑距离。通过实验确定事件序列距离对于整个测试用例距离的影响并确定其权重。最后设计实验与随机测试方法进行比较说明了方法的有效性。