随着计算机应用的日益普及和深入，软件系统的规模和复杂性不断增大，研制可信软件技术以提高软件系统的质量已经成为十分重要和迫切的需求。　　 软件开发生命周期可以分为需求分析、设计、实现、测试和发布等多个阶段，在开发过程的不同阶段中创建的软件制品主要包括模型和代码，这两者是对系统不同层次的抽象，软件开发过程就是构造模型并在此基础上最终实现代码的过程。可信软件技术涉及软件分析、测试、验证、监控和容错等多个方面，其应用贯穿于整个软件开发生命周期，本文针对软件模型和代码，重点研究形式验证、精化、监控和容错等相关技术。　　 在软件开发过程中，模型是需求分析阶段和设计阶段的重要制品。确保需求模型和设计模型之间的一致性，这是本文关注的第一个问题(模型级)。本文关注Web服务领域中服务需求模型和设计模型之间的消息流一致性验证问题。　　 在软件开发过程中，模型转换是构造模型的重要途径，前一步模型是生成后一步模型的基础，保证转换前后模型的一致性(即模型转换的正确性)是软件开发中的重要问题。本文在为对象和构件系统提供形式建模支持的前提下，研究了支持正确模型转换的有效实现，这是本文关注的第二个问题(模型级)。　　 从模型到代码的转换和生成是一个从高层抽象到低层实现的映射过程，软件在模型级是可信任的并不说明其在代码级也是可信任的，为此需要在软件开发过程中加入针对代码的分析、测试和验证活动。然而，针对代码的分析、测试和验证活动经常受到代码规模和复杂性的制约，因此在软件运行阶段增加监控和容错手段是提高系统可信性的有效途径，这是本文关注的第三个问题(代码级)。　　 本文围绕上述问题展开研究工作，具体内容和结果如下：　　 1.面向Web服务的建模与验证。采用UML顺序图构成基于场景的规约、WS-BPEL作为Web服务的描述语言，提出了一种面向基于场景规约对Web服务消息流进行分析与验证的方法：首先，对WS-BPEL消息流进行分析并将其自动抽象为基于Petri网的模型；同时，为了缩小状态空间、提高验证效率，在不影响消息交互顺序的前提下，对WS-BPEL源码和基于Petri网的模型分别进行化简，即面向基于场景规约将与验证无关的活动和元素删除；最后，通过遍历基于Petri网的模型来验证WS-BPEL消息流与基于场景的规约之间的一致性(消息交互顺序的存在/强制一致性)。　　 2.对象和构件系统形式模型的转换实现。在模型驱动的软件系统开发中，开发过程是一个渐进的增量式过程，软件系统的开发过程是由一系列构造正确模型并保证模型转换正确性的步骤组成的。保证模型转换的正确性是软件开发中的重要问题，本文关注的是模型转换中不同抽象层次之间模型的一致性。关系演算rCOS能够为对象和构件系统提供形式建模支持并证明模型转换的正确性，这是本文工作的理论基础。在总结基于rCOS模型的开发过程的基础上，实现了基于元模型的模型转换架构，并使用模型转换语言QVT来实现经rCOS证明的正确的模型转换。　　 3.基于多核平台的软件监控与容错途径和工具支撑。在总结软件监控和容错基本原理的基础上，提出基于多核平台的软件监控和容错途径，并给出其实现框架。在该框架下，监控和容错任务通过多线程技术来实现，并通过操作系统提供的语言API接口映射分配到不同的核上运行。进一步开发了工具McC++/Java使得上述途径和框架能够在C++/Java中得以实现。McC++/Java通过在C++/Java中引入专用注释标记支持自动地向多核平台映射分配监控和容错任务，从而在C++/Java程序中屏蔽了向多核平台映射分配监控和容错任务的技术细节，减轻了软件开发人员的负担，提高了相应的编程效率。