问题框架中问题领域因果行为的形式化验证

为问题框架中问题渐变所依赖的问题领域因果行为的确立提出一种形式化验证方法。为了对问题渐变过程中事件间的因果关系提供可验证的证据支持,简化问题表征的复杂度,进而提高计算机领域软件规约的可靠性,采纳了一种基于NuSMV语言的符号模型检验的形式化验证方法。该验证方法采用UML状态机表示问题领域内部状态变化的有限结构空间,用CTL公式描述问题域内状态之间的可达性性质,通过遍历有限结构状态机来检验CTL公式的正确性,筛选出具有因果关系的外部共享事件,为问题渐变提供有效的技术支持。

时空大数据资源集成框架设计与应用

随着地理空间信息技术的快速发展,产生了大量形式各异的时空数据资源与服务应用。针对资源共享存在的服务互操作、消息传输、数据同步和数据传输等技术瓶颈问题,提出一种时空大数据资源集成框架(STDRIF)。采用松耦合模块化的方式,形成一套从数据资源集成到服务调用的完整技术体制,可以有效整合各类时空数据资源。以J2EE架构应用为例,验证了STDRIF的可用性并进行性能分析。实验结果表明,STDRIF具有较高的性能和良好的用户体验。