==== Systems of Systems Architecture Models Stochastic Verification ====
A. Mohsin, N. K. Janjua, S. M. S. Islam and M. A. Babar, "SAM-SoS: A Stochastic Software Architecture Modeling and Verification Approach for Complex System-of-Systems," in IEEE Access, vol. 8, pp. 177580-177603, 2020, doi: 10.1109/ACCESS.2020.3025934.
**** Fire Monitoring and Emergency Response SoS (FM-ERSoS) model checking from architectual specificaiton ****
Open PRISM and press Model tab and then Open Model
Model Capabilities
Steady-state Analysis Transient Anaysis Known bounds and unkown bounds Deadlock and liveliness
-
Download the model files and properties files first Select the model FMERSoS from Model and then click open Model
-
Then load the model and click on load model by click sub-tab withn Model Menu
-
Check States, Transitions and intial states of CSs within Model
-
Calcualte steady state probabilities with known bonds and unkonwn bounds
-
Check transition rewards and state rewards
-
Change the model parameters as per needs
-
you can test multiple models seperately for experimentation of complex system stochastic behavior analsis
-
Feel free to modify the models as per needs
-
Models can be modified considering the Real-Time System needs in the domains of Complex Systems (Smart Cities consisting of IoTs,Cyber-Physical SoS, smart grids, Critical Infrastructure) where Software Components are main drivers with operational and managerial indpendence.
-
Performance and Reliability metrics and sub-metrics are calculated with SoS stochastic system dynamics, hower other core Quality Attributes such as Security, Availibility could be evaluated with contextual modifications in models and properites.
******* See the model how varsious constraints in relation to the SoS Architecture are applied *******
********** Experimentation of CTMC FM-ERSoS Models **********
- Load the model first by following above steps
- Load properites file in CSL that you have downloaded
- Start experimentaitons with properties specification one by one
- Evaluate steady state liklihoods with properties in experiments
- Evalualte Transient liklihoods to measure Performance and Reliability of FM-ERSoS