ソフトウェアシステムの開発において仕様記述は重要な工程であり，仕様記述の曖昧さや誤りは開発全体の生産性および信頼性に重大な影響を与えることが知られている.形式仕様を記述することはモデリングの一種であり，数学的な裏付けのある道具立てによつて適切な抽象度でシステムの機能を厳密に定義する工程である.厳密で適切な抽象度の仕様記述を得るために，形式仕様記述者は仕様記述の初期段階において問題領域を探索し対象ドメィンの知識獲得や要求項目への理解を深めながらモデリングを進める.本論文では，探索的なモデリングを支援するためのツールに求められる性質を示した上で.形式仕様記述言語VDM-SLによる探索的モデリングを支援する統合開発環境ViennaTalkのデザィン指針，設計および実装を示す.%EV3RT is, to our knowledge, the first RTOS-based software platform for LEGO Mindstorms EV3 robotics kit. It is faster and more suitable for developing applications with real-time requirements than other existing software platforms. In practice, EV3RT has been selected as one of the officially supported platforms of ET Robocon, a popular robot competition in Japan, since 2015 and used by many participating teams to make their robots accomplish the assigned tasks more stably and precisely. In this paper, the usage and architecture of EV3RT are firstly introduced. We then explain TOPPERS/HRP2 kernel, the RTOS of EV3RT, and how to use its protection functionalities to build a reliable platform. A mechanism to support dynamic module loading in a static RTOS is proposed to implement the application loader for EV3RT. Implementation techniques like approach to reusing Linux device drivers are also described. Finally, the advantages of EV3RT are shown by evaluating and comparing its performance with other platforms.
展开▼
