高可信软件工程对目前的软件理论和技术提出了严峻的挑战，涉及到一系列科学问题。

第一，软件系统的行为特征。如何定性/定量地描述软件的行为？如何建立各类复杂的软件结构和系统对应的系统行为？这是软件理论的基本问题。软件的静态语法与其动态语义的分离是造成软件行为难于描述和推理的原因。随着软件规模的增大，软件中并发、实时、分布、移动等特性的出现，这些问题的认识亟待深入。

第二，软件可信性质与软件行为的关系。如何描述软件可信性质及其软件行为的关系？我们看到，上述关于软件可信性质的描述是非形式化的抽象陈述。必须建立起性质和软件行为之间的内在联系及其严格的描述，才能在软件开发环境中，设计并验证所需的可信性质。

第三，面对软件可信性质的设计和推理。如何将软件可信性质（通常非操作性的）融入软件设计（操作性）？可信性质通常是软件系统的全局约束，伴随着软件开发过程逐步地“设计”出来，最终获得这些可信性质。如何针对可信性质发现一种分而治之的策略从而控制复杂性，是进行面向可信性质的软件设计和验证的关键。

第四，软件系统的可信性质的确认。如何发现和评估软件系统是否具有可信性质？量化是一种工程科学成熟的重要标志，需要对软件可信性质有合适的度量方法，并能在软件过程中进行跟踪。