我々は現在までに、Javaのための振舞インターフェース仕様記述言語Moxaを開発してきた。MoxaはJava Modeling Language (JML)を拡張したものであり、表明アスペクトと呼ばれる機構を用いて表明間を横断する性質を分離することで、長大で複雑になりがちな実アプリケーションの仕様のモジュール化を可能にしている。本稿ではまずMoxaの設計について簡単に説明した後、その拡張-プロトコルにもとづくアスペクト記述-について議論する。この拡張は、メソッド呼び出し系列(プロトコル)にもとづいた仕様の記述・テスト・検証を容易にするためのものである。 We have been developing Moxa, a behavioral interface specification language tailord for Java. Moxa provides a new modularization mechanism called assertion aspect that can capture the crosscutting properties among assertions in a specification. Using this mechanism, we can modularize large and complex specification of real-world applications. In this paper, we briefly explain the design of Moxa and then discuss its extension called protocoloriented aspect description. The extension provides convenient way to describe, test and verify specifications that are described based on method invocation sequence.