TY - GEN
T1 - VeriSiMPL
T2 - 10th International Conference on Quantitative Evaluation of Systems, QEST 2013
AU - Adzkiya, Dieky
AU - Abate, Alessandro
N1 - Funding Information:
This research is funded by the European Commission under the MoVeS project, FP7-ICT-2009-5 257005, by the European Commission under the NoE FP7-ICT-2009-5 257462, by the European Commission under Marie Curie grant MANTRAS PIRG-GA-2009-249295, and by NWO under VENI grant 016.103.020.
PY - 2013
Y1 - 2013
N2 - VeriSiMPL ("very simple") is a software tool to obtain finite abstractions of Max-Plus-Linear (MPL) models. MPL models (Sect. 2), specified in MATLAB, are abstracted to Labeled Transition Systems (LTS). The LTS abstraction is formally put in relationship with the concrete MPL model via a (bi)simulation relation. The abstraction procedure (Sect. 3) runs in MATLAB and leverages sparse representations, fast manipulations based on vector calculus, and optimized data structures such as Difference-Bound Matrices. LTS abstractions can be exported to structures defined in the PROMELA. This enables the verification of MPL models against temporal specifications within the SPIN model checker (Sect. 4). The toolbox is available at http://sourceforge.net/ projects/verisimpl/.
AB - VeriSiMPL ("very simple") is a software tool to obtain finite abstractions of Max-Plus-Linear (MPL) models. MPL models (Sect. 2), specified in MATLAB, are abstracted to Labeled Transition Systems (LTS). The LTS abstraction is formally put in relationship with the concrete MPL model via a (bi)simulation relation. The abstraction procedure (Sect. 3) runs in MATLAB and leverages sparse representations, fast manipulations based on vector calculus, and optimized data structures such as Difference-Bound Matrices. LTS abstractions can be exported to structures defined in the PROMELA. This enables the verification of MPL models against temporal specifications within the SPIN model checker (Sect. 4). The toolbox is available at http://sourceforge.net/ projects/verisimpl/.
UR - http://www.scopus.com/inward/record.url?scp=84882794971&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40196-1_22
DO - 10.1007/978-3-642-40196-1_22
M3 - Conference contribution
AN - SCOPUS:84882794971
SN - 9783642401954
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 274
EP - 277
BT - Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Proceedings
Y2 - 27 August 2013 through 30 August 2013
ER -