Skip to content

Latest commit

 

History

History
84 lines (62 loc) · 2.4 KB

README.MacOS.ja.md

File metadata and controls

84 lines (62 loc) · 2.4 KB
Raw

ChibiOS/RTのVeriFastによる検証 (MacOS版)

ChibiOS/RT上で動作するアプリケーションをVeriFastで検証します。

開発環境の構築

関連パッケージをインストールしてください。

$ brew tap PX4/homebrew-px4
$ brew update
$ brew install wget git gcc-arm-none-eabi cmake picocom libusb

stlinkをダウンロードしてビルドしてください。

$ git clone https://github.com/texane/stlink.git
$ (cd stlink && make)
$ (cd stlink/build/Release && sudo make install)

VeriFastの最新版をダウンロードし、展開してPATHを通してください。

$ wget http://82076e0e62875f063ae8-929808a701855dfb71539d0a4342d4be.r54.cf5.rackcdn.com/verifast-nightly-osx.tar.gz
$ tar xf verifast-nightly-osx.tar.gz
$ mv verifast-*/ verifast
$ export PATH=`pwd`/verifast/bin:$PATH

本ソースコードをダウンロードしてください。

$ git clone https://github.com/fpiot/chibios-verifast.git

ChibiOSアプリケーションのビルド

ソースコードをビルドしてください。

$ cd chibios-verifast/verifast_demo/STM32/RT-STM32F091RC-NUCLEO
$ make

ChibiOSアプリケーションの実行

ボードとMacをUSBケーブルで接続した後、ファームウェアを書き込みます。

$ cd chibios-verifast/verifast_demo/STM32/RT-STM32F091RC-NUCLEO
$ make flash

シリアルコンソールを開いた後、ボードのUSERスイッチを押下してください。以下のようなログが表示されます。

$ picocom -b 9600 /dev/tty.usbmodem1423
picocom v1.7
--snip--
Terminal ready

*** ChibiOS/RT test suite
***
*** Kernel:       3.1.5
*** Compiled:     Jan 15 2017 - 20:38:01
*** Compiler:     GCC 4.8.4 20140725 (release) [ARM/embedded-4_8-branch revision 213147]
*** Architecture: ARMv6-M
*** Core Variant: Cortex-M0
*** Port Info:    Preemption through NMI
*** Platform:     STM32F091xC Entry Level Access Line devices
*** Test Board:   STMicroelectronics NUCLEO-F091RC
--snip--

ChibiOSアプリケーションの検証

VeriFastでソースコードを検証するには、以下のようにしてVeriFast IDEを起動してください。

$ cd chibios-verifast/verifast_demo/STM32/RT-STM32F091RC-NUCLEO
$ make vfide