基于层次化时间STM软件设计的形式化验证

状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的程序建模语言。事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用。文中针对这些问题,首先提出层次化时间状态迁移矩阵(Hierarchical Time State Transition Matrix,HTSTM)模型,用于设计、建模和验证具有时间条件约束的软件系统,并给出形式化表示方法。基于该表示方法提出一种符号化编码方法,采用有界模型检测思想将需要验证的LTL性质输入SMT(Satisfiability Modulo Theories)求解器进行验证,从而在一定程度上证明了软件设计的正确性。

一种解决嵌入式软件并发缺陷的建模方法

嵌入式并发软件的中断嵌套和线程交织等程序的随机性和不确定性(Randomicity and Nondeterminism)会引起数据竞争(Data Race)和原子性违背(Atomicity Violations)等并发缺陷问题,并且这些问题很难被修复和重新构建。针对嵌入式软件中的数据竞争和原子性违背这类并发缺陷问题,文中提出了瘦中断处理(Thin Interrupt Service Routine,Thin ISR)方式。首先,利用状态迁移矩阵(State Transition Matrix,STM)进行建模,把中断处理程序中与访问共享变量相关的程序段移植到主程序中,即中断处理程序只负责将外界中断请求数据存到缓冲区中,中断的具体处理由主程序完成;然后,利用构建的STM模型生成对应的C代码,这样可以有效地避免原子性违背和数据竞争等并发缺陷;最后,利用排队方法对中断的到达时间与离开时间进行仿真。实验结果验证了本方法在解决数据竞争和原子性违背等并发缺陷问题方面的可行性与有效性。

Android智能电视测试用例生成方法及应用研究

相比传统电视,由于增加上网浏览、音视频文件播放、下载各种应用软件等多种功能,智能电视系统软硬件变得异常复杂,用户使用相对繁琐,这种大批量消费类产品的可靠性是目前智能电视厂家面临的主要问题。提出根据系统设计规格书对智能电视的操作行为采用AutoStar进行层次化状态迁移矩阵(STM)建模,进而转化为具有记忆功能的正则表达式,同时根据正则表达式圈复杂度来递归确定正则表达式中包含所有闭包循环的次数,并生成测试用例,自动转成Python脚本,通过Android提供的ADB接口发送给Android智能电视,最后设计实现Android智能电视测试平台,该平台应用于国内智能电视的测试。