随着信息化与工业化进程的不断融合，应用于航空航天、武器装备、医疗设备、工业控制、汽车电子、金融政务等诸多国家关键信息领域的任务关键系统，广泛的采用了多线程、多处理器、分布式等信息技术来提高其处理能力，并且逐渐转到开放的互联网环境中来，与此同时也引入了大量的复杂性、不确定性和安全性问题。这类系统易吸引外部敌对势力和内部渗透人员的强烈关注和破坏，其功能一旦失效将会引起灾难性的后果。建立一个有效的行为分析与检测模型，是解决这类系统安全问题的重要手段之一，已经成为当前信息安全领域的热点。但是，现有的行为建模与检测技术在如何精确地描述并发行为、如何消减状态空间以降低建模的复杂度等方面还存在不足。针对这些问题，本文的主要研究工作如下。首先，针对现有行为模型不能有效描述行为的并发特征的问题，提出一种基于进程代数的软件行为形式化描述及映射机制。利用可执行代码分析及控制流重构技术，给出从可执行代码中采集控制流和数据流等软件行为信息的方法。依据进程代数的语法语义及进程等价概念，给出从采集到的行为信息到进程代数的映射方法，从而建立起软件行为与进程代数语义的对应关系，奠定了软件行为向代数系统的代入和演算的基础。其次，针对现有行为模型在函数合并过程中引入不确定性的问题，提出一种基于进程代数和系统调用的顺序行为分析与检测方法。该方法针对不存在并发的顺序行为，给出了利用代数性质和运算法则合并各单函数进程表达式得到全局进程表达式的算法，避免了基于自动机的行为模型引入不确定性的不足，有效地提高了行为模型的精确性和效率。给出了行为检测规则和检测算法，通过对控制流、数据流攻击的检测，验证了行为模型的有效性。再次，针对现有行为检测模型无法有效地表示和检测多线程程序中的并发行为的问题，给出了一种面向多线程的并发行为分析和检测方法。给出了并发表示法则，形式化的描述了多线程之间的互斥与同步等关系。并通过理论分析和实验验证，论证了该方法的精确性和效率。然后，充分考虑任务关键系统中广泛应用分布式技术所引入的并发性问题，提出了一种面向分布式并发行为的分析和检测方法。利用进程代数具有的代数性质，消除了进程表达式的不确定性、添加了并发操作，准确描述了多主机节点之间通信与协作的并发性特征。构造了同步进程集和运行时状态集，进而给出了迁移法则和检测方法，并通过实验论证了该方法的时空效率。最后，通过对一个地铁自动控制模拟系统的案例分析，给出行为建模和检测的步骤、模型的总体框架、部署方案以及对攻击的应对。阐述了本文所提出的行为检测模型在任务关键系统中的应用情况。