GitHub - Claydelas/formal-methods: Formal model and verification of a multi-cabin elevator system in Event-B/Rodin, with additional static verification in Ada/SPARK (not in repo), following a requirement specification.

Claydelas / formal-methods Public

Notifications You must be signed in to change notification settings
Fork 1
Star 1

Formal model and verification of a multi-cabin elevator system in Event-B/Rodin, with additional static verification in Ada/SPARK (not in repo), following a requirement specification.

1 star 1 fork Branches Tags Activity

Star

Notifications

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 12 Commits
.project		.project
m0_cabins.bcm		m0_cabins.bcm
m0_cabins.bpo		m0_cabins.bpo
m0_cabins.bpr		m0_cabins.bpr
m0_cabins.bps		m0_cabins.bps
m0_cabins.bum		m0_cabins.bum
m0_cabins_context.bcc		m0_cabins_context.bcc
m0_cabins_context.bpo		m0_cabins_context.bpo
m0_cabins_context.bpr		m0_cabins_context.bpr
m0_cabins_context.bps		m0_cabins_context.bps
m0_cabins_context.buc		m0_cabins_context.buc
m0_cabins_old1.bpr		m0_cabins_old1.bpr
m1_shafts.bcm		m1_shafts.bcm
m1_shafts.bpo		m1_shafts.bpo
m1_shafts.bpr		m1_shafts.bpr
m1_shafts.bps		m1_shafts.bps
m1_shafts.bum		m1_shafts.bum
m1_shafts_alt_context.bpr		m1_shafts_alt_context.bpr
m1_shafts_context.bcc		m1_shafts_context.bcc
m1_shafts_context.bpo		m1_shafts_context.bpo
m1_shafts_context.bpr		m1_shafts_context.bpr
m1_shafts_context.bps		m1_shafts_context.bps
m1_shafts_context.buc		m1_shafts_context.buc
m1_shafts_old1.bpr		m1_shafts_old1.bpr
m1_shafts_old2.bpr		m1_shafts_old2.bpr
m2_motor.bcm		m2_motor.bcm
m2_motor.bpo		m2_motor.bpo
m2_motor.bpr		m2_motor.bpr
m2_motor.bps		m2_motor.bps
m2_motor.bum		m2_motor.bum
m2_motor_context.bcc		m2_motor_context.bcc
m2_motor_context.bpo		m2_motor_context.bpo
m2_motor_context.bpr		m2_motor_context.bpr
m2_motor_context.bps		m2_motor_context.bps
m2_motor_context.buc		m2_motor_context.buc
m3_door.bcm		m3_door.bcm
m3_door.bpo		m3_door.bpo
m3_door.bpr		m3_door.bpr
m3_door.bps		m3_door.bps
m3_door.bum		m3_door.bum
m3_door_context.bcc		m3_door_context.bcc
m3_door_context.bpo		m3_door_context.bpo
m3_door_context.bpr		m3_door_context.bpr
m3_door_context.bps		m3_door_context.bps
m3_door_context.buc		m3_door_context.buc
m4_buttons.bcm		m4_buttons.bcm
m4_buttons.bpo		m4_buttons.bpo
m4_buttons.bpr		m4_buttons.bpr
m4_buttons.bps		m4_buttons.bps
m4_buttons.bum		m4_buttons.bum
m4_buttons_context.bcc		m4_buttons_context.bcc
m4_buttons_context.bpo		m4_buttons_context.bpo
m4_buttons_context.bpr		m4_buttons_context.bpr
m4_buttons_context.bps		m4_buttons_context.bps
m4_buttons_context.buc		m4_buttons_context.buc
m5_impl.bcm		m5_impl.bcm
m5_impl.bpo		m5_impl.bpo
m5_impl.bpr		m5_impl.bpr
m5_impl.bps		m5_impl.bps
m5_impl.bum		m5_impl.bum
m5_impl_context.bcc		m5_impl_context.bcc
m5_impl_context.bpo		m5_impl_context.bpo
m5_impl_context.bpr		m5_impl_context.bpr
m5_impl_context.bps		m5_impl_context.bps
m5_impl_context.buc		m5_impl_context.buc

About

Formal model and verification of a multi-cabin elevator system in Event-B/Rodin, with additional static verification in Ada/SPARK (not in repo), following a requirement specification.

formal-methods rodin event-b

Activity

1 star

2 watching

1 fork

Report repository