提升移动应用的可靠性

Android平台由Google于2008年推出，作为移动设备的操作系统。Android的SDK为编程提供了广泛支持以及大量示例和文档。可靠性是智能手机应用日益关注的问题，因为它们通常包含个人信息和数据。因此，需要用于检查应用正确行为的技术和工具。本文展示了如何使用Event-B方法对Android应用的设计进行推理和验证，以及如何利用它来记录实现决策。我们的方法包括在Event-B中对应用的核心功能进行建模，并利用所生成的证明义务（Proof Obligations）所提供的证据来对应用的设计与实现进行推理。尽管我们未提出新方法，但我们证明了带有Event-B的重量级形式化方法（FMs）技术可有效用于支持正确Android应用的开发。我们给出一个案例研究，其中我们在Event-B中设计WhatsApp的核心功能，将其编码在三个机器精化（machine refinements）上，分别建模基本功能（聊天、删除内容、转发内容、删除聊天会话等）、聊天会话的已读和未读状态，以及实现细节。我们报告并讨论了核心功能设计与实现中的潜在挑战。