Formal Verification of a Block chain-enabled Smart Learning Environment Framework using Petri NETs

Abstract

Smart learning is a technology-enhanced learning system that is effective, efficient, engaging
style of learning. Smart Learning Environment (SLE) is the physical learning environment that
supports context aware ubiquitous learning by using sophisticated technologies. The existing
Learning Technology Systems Architectures (Frameworks) need to be redesigned to integrate the
sophisticated technologies. The enhanced frameworks must reach the higher levels of smartness.
The "Smartness levels" are a measure to assess the learning environments. While achieving the
higher smart levels, a formal verification of the proposed architectures is required to confirm the
smartness levels attained. It is significant as these frameworks are used as reference models for
the development of the Learning Management Systems. A Scenario based formal verification
procedure of an SLE is proposed in this paper. The formal verification procedure includes
representing the a scenario into an activity diagram which is then converted to a Petrinet that is
helpful in performing Matrix analysis, Reachability graph analysis, Generalized Stochastic Petri
Nets(GSPN) analysis, Simulation, and State-space analysis. For the latest Blockchain enabled
SLE framework, an algorithm for online examination scenario is proposed. As this frameworks
has more secured mechanism than traditional frameworks, the standardization challenge
"security" which is at first two levels of SLE Smartness is addressed. The proposed Algorithm
is formally validated using the proposed procedure using petri nets..