{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:44:18Z","timestamp":1742384658223},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2010,5,9]],"date-time":"2010-05-09T00:00:00Z","timestamp":1273363200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1007\/s10009-010-0156-8","type":"journal-article","created":{"date-parts":[[2010,5,8]],"date-time":"2010-05-08T12:12:00Z","timestamp":1273320720000},"page":"391-403","source":"Crossref","is-referenced-by-count":50,"title":["Oris: a tool for modeling, verification and evaluation of real-time systems"],"prefix":"10.1007","volume":"12","author":[{"given":"Giacomo","family":"Bucci","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laura","family":"Carnevali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lorenzo","family":"Ridi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Vicario","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,5,9]]},"reference":[{"key":"156_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: 17th ICALP (1990)","DOI":"10.1007\/BFb0032042"},{"key":"156_CR2","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL: a tool-suite for automatic verification of real-time systems. In: Hybrid Systems III: LNCS, 1066 (1996)"},{"key":"156_CR3","unstructured":"Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool KRONOS. In: Hybrid Systems III, 1066. Springer (1995)"},{"issue":"9","key":"156_CR4","doi-asserted-by":"crossref","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","volume":"24","author":"P. Merlin","year":"1976","unstructured":"Merlin P., Farber D.: Recoverability of communication protocols. IEEE Trans. Commun. 24(9), 1036\u20131043 (1976)","journal-title":"IEEE Trans. Commun."},{"issue":"3","key":"156_CR5","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"Berthomieu B., Diaz M.: Modeling and verification of time dependent systems using time petri nets. IEEE Trans. Softw. Eng. 17(3), 259\u2013273 (1991)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"156_CR6","doi-asserted-by":"crossref","first-page":"728","DOI":"10.1109\/32.940727","volume":"27","author":"E. Vicario","year":"2001","unstructured":"Vicario E.: Static analysis and dynamic steering of time dependent systems using Time Petri Nets. IEEE Trans. Softw. Eng. 27(1), 728\u2013748 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"156_CR7","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1109\/TSE.2004.1265815","volume":"30","author":"G. Bucci","year":"2004","unstructured":"Bucci G., Fedeli A., Sassoli L., Vicario E.: Timed state space analysis of real time preemptive systems. IEEE Trans. Softw. Eng. 30(2), 97\u2013111 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"156_CR8","doi-asserted-by":"crossref","unstructured":"Altisen, K., Gossler, G., Pnueli, A., Sifakis, J., Tripakis, S., Yovine, S.: A framework for scheduler synthesis. In: RTSS \u201999: Proceedings of the 20th IEEE Real-Time Systems Symposium, Washington, DC, USA, 154\u00a0pp. IEEE Computer Society (1999)","DOI":"10.1109\/REAL.1999.818838"},{"key":"156_CR9","unstructured":"Bertin, V., Closse, E., Poize, M., Pulou, J., Sifakis, J., Venier, P., Weil, D., Yovine, S.: Taxys = Esterel + Kronos. A tool for verifying real-time properties of embedded systems. In: CDC \u201901: Proceedings of the 40th IEEE Conference on Decision and Control (2001)"},{"key":"156_CR10","doi-asserted-by":"crossref","unstructured":"Kloukinas, C., Yovine, S.: Synthesis of safe, QoS extendible, application specific schedulers for heterogeneous real-time systems. In: In ECRTS 03: Euromicro Conference on Real-Time Systems, pp. 287\u2013294. IEEE Computer Society Press (2003)","DOI":"10.1109\/EMRTS.2003.1212754"},{"key":"156_CR11","doi-asserted-by":"crossref","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES: a tool for schedulability analysis and code generation of real-time systems. In: Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems (2003)","DOI":"10.1007\/978-3-540-40903-8_6"},{"key":"156_CR12","doi-asserted-by":"crossref","unstructured":"Gardey, G., Lime, D., Magnin, M., Roux, O.: Rom\u00e9o: a tool for analyzing time petri nets. In: 17th International Conference on Computer Aided Verification (CAV\u0107605). Lecture Notes in Computer Science (2005)","DOI":"10.1007\/11513988_41"},{"issue":"14","key":"156_CR13","doi-asserted-by":"crossref","first-page":"2741","DOI":"10.1080\/00207540412331312688","volume":"42","author":"B. Berthomieu","year":"2004","unstructured":"Berthomieu B., Ribet P.O., Vernadat F.: The tool TINA\u2014construction of abstract state spaces for petri nets and time petri nets. Int. J. Prod. Res. 42(14), 2741\u20132756 (2004)","journal-title":"Int. J. Prod. Res."},{"key":"156_CR14","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer-Verlag (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"156_CR15","first-page":"460","volume":"2280","author":"T. Amnell","year":"2002","unstructured":"Amnell T., Fersman E., Mokrushin L., Pettersson P., Yi W.: Times\u2014a tool for modelling and implementation of embedded systems. LNCS 2280, 460\u2013464 (2002)","journal-title":"LNCS"},{"key":"156_CR16","doi-asserted-by":"crossref","unstructured":"Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Modeling flexible real time systems with preemptive Time Petri Nets. In: Proceedings of the 15th Euromicro Conference on Real-Time Systems (ECRTS03) (2003)","DOI":"10.1109\/EMRTS.2003.1212753"},{"issue":"5","key":"156_CR17","doi-asserted-by":"crossref","first-page":"703","DOI":"10.1109\/TSE.2009.36","volume":"35","author":"E. Vicario","year":"2009","unstructured":"Vicario E., Sassoli L., Carnevali L.: Using stochastic state classes in quantitative evaluation of dense-time reactive systems. IEEE Trans. Softw. Eng. 35(5), 703\u2013719 (2009)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"156_CR18","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1109\/TSE.2008.101","volume":"35","author":"L. Carnevali","year":"2009","unstructured":"Carnevali L., Grassi L., Vicario E.: State-density functions over DBM domains in the analysis of non-Markovian models. IEEE Trans. Softw. Eng. 35(2), 178\u2013194 (2009)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"156_CR19","doi-asserted-by":"crossref","unstructured":"Horv\u00e1th, A., Vicario, E.: Aggregated stochastic state classes in quantitative evaluation of non-markovian Stochastic Petri Nets. In: Proceedings of the 6th Int. Conf. on Quant. Evaluation of Sys. (QEST \u201909) (2009)","DOI":"10.1109\/QEST.2009.33"},{"key":"156_CR20","doi-asserted-by":"crossref","unstructured":"Sassoli, L., Vicario, E.: Close form derivation of state-density functions over DBM domains in the analysis of non-Markovian models. In: Proc. of the 4th Int. Conf. on the Quant. Evaluation of Sys. (QEST) (2007)","DOI":"10.1109\/QEST.2007.23"},{"key":"156_CR21","doi-asserted-by":"crossref","unstructured":"Bucci, G., Piovosi, R., Sassoli, L., Vicario, E.: Introducing probability within state class analysis of dense time dependent systems. In: Proc. of the 2nd Int. Conf. on Quant. Evaluation of Sys. (QEST \u201905) (2005)","DOI":"10.1109\/QEST.2005.17"},{"key":"156_CR22","unstructured":"Carnevali, L., Ridi, L., Vicario, E.: Partial stochastic characterization of timed runs over DBM domains. In: Proc. of the 9th International Workshop on Performability Modeling of Computer and Communication Systems (2009)"},{"key":"156_CR23","doi-asserted-by":"crossref","unstructured":"Cassez, F., Larsen, K.G.: The Impressive Power of Stopwatches. LNCS, vol. 1877 (August, 2000)","DOI":"10.1007\/3-540-44618-4_12"},{"key":"156_CR24","doi-asserted-by":"crossref","unstructured":"Roux, O.H., Lime, D.: Time petri nets with inhibitor hyperarcs: formal semantics and state-space computation. In: 25th Int. Conf. on Theory and Application of Petri nets, vol. 3099, pp. 371\u2013390 (2004)","DOI":"10.1007\/978-3-540-27793-4_21"},{"key":"156_CR25","doi-asserted-by":"crossref","unstructured":"Carnevali, L., Grassi, L., Vicario, E.: A tailored V-Model exploiting the theory of preemptive Time Petri Nets. In: Ada-Europe \u201908: Proc. of the Ada-Europe Int. Conf. on Reliable Software Technologies, pp. 87\u2013100. Springer-Verlag, Berlin (2008)","DOI":"10.1007\/978-3-540-68624-8_7"},{"key":"156_CR26","doi-asserted-by":"crossref","unstructured":"Carnevali, L., Sassoli, L., Vicario, E.: Sensitization of symbolic runs in real-time testing using the ORIS tool. In: Proc. of the IEEE Conf. on Emerging Technologies and Factory Automation (ETFA) (2007)","DOI":"10.1109\/EFTA.2007.4416757"},{"key":"156_CR27","doi-asserted-by":"crossref","unstructured":"Carnevali, L., Sassoli, L., Vicario, E.: Casting preemptive Time Petri Nets in the development life cycle of real-time software. In: Proc. of the Euromicro Conference on Real-Time Systems (2007)","DOI":"10.1109\/ECRTS.2007.86"},{"issue":"11","key":"156_CR28","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1109\/TSE.2005.122","volume":"31","author":"G. Bucci","year":"2005","unstructured":"Bucci G., Sassoli L., Vicario E.: Correctness verification and performance analysis of real time systems using stochastic preemptive Time Petri Nets. IEEE Trans. Softw. Eng. 31(11), 913\u2013927 (2005)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"156_CR29","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1006\/jvlc.2001.0214","volume":"12","author":"E. Vicario","year":"2001","unstructured":"Vicario E.: Engineering the usability of a visual formalism for real-time temporal logic. J. Vis. Lang. Comput. 12(6), 573\u2013599 (2001)","journal-title":"J. Vis. Lang. Comput."},{"key":"156_CR30","doi-asserted-by":"crossref","unstructured":"Lusini, M., Vicario, E.: Design and evaluation of a visual formalism for real time logics. In: ACoS \u201998\/VISUAL \u201998, AIN \u201997: Selected Papers on Services and Visualization: Towards User-Friendly Design, pp. 158\u2013173. Springer-Verlag, London (1998)","DOI":"10.1007\/BFb0053504"},{"key":"156_CR31","doi-asserted-by":"crossref","unstructured":"Carnevali, L., D\u2019Amico, D., Ridi, L., Vicario, E.: Automatic code generation from real-time systems specifications. In: Proceedings of the IEEE\/IFIP International Symposium on Rapid System Prototyping (RSP) (2009)","DOI":"10.1109\/RSP.2009.24"},{"key":"156_CR32","unstructured":"Dept. of Aerospace Eng. of the Polytechnic of Milan: RTAI: Real Time Application Interface for Linux. https:\/\/www.rtai.org"},{"issue":"9","key":"156_CR33","doi-asserted-by":"crossref","first-page":"1175","DOI":"10.1109\/12.57058","volume":"39","author":"L. Sha","year":"1990","unstructured":"Sha L., Rajkumar R., Lehoczky J.P.: Priority inheritance protocols: an approach to real-time synchronization. IEEE Trans. Comput. 39(9), 1175\u20131185 (1990)","journal-title":"IEEE Trans. Comput."},{"key":"156_CR34","unstructured":"Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In Mason, R.E.A. (ed.) Information Processing: Proceedings of the IFIP Congress 1983, vol. 9, pp. 41\u201346. Elsevier (1983)"},{"key":"156_CR35","doi-asserted-by":"crossref","unstructured":"Dill, D.: Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of Workshop on Computer Aided Verification Methods for Finite State Systems (1989)","DOI":"10.1007\/3-540-52148-8_17"},{"issue":"2","key":"156_CR36","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke E.M., Emerson E.A., Sistla A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"7","key":"156_CR37","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1016\/0169-7552(93)90047-8","volume":"25","author":"R. De Nicola","year":"1993","unstructured":"De Nicola R., Fantechi A., Gnesi S., Ristori G.: An action-based framework for verifying logical and behavioural properties of concurrent systems. Comput. Netw. ISDN Syst. 25(7), 761\u2013778 (1993)","journal-title":"Comput. Netw. ISDN Syst."},{"key":"156_CR38","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Logics and models of real-time: a survey. In: Real Time: Theory in Practice, vol. 600, pp. 74\u2013106. Springer-Verlag (1991)","DOI":"10.1007\/BFb0031988"},{"issue":"3","key":"156_CR39","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1347375.1347389","volume":"7","author":"R. Wilhelm","year":"2008","unstructured":"Wilhelm R., Engblom J., Ermedahl A., Holsti N., Thesing S., Whalley D., Bernat G., Ferdinand C., Heckmann R., Mitra T., Mueller F., Puaut I., Puschner P., Statshulat J., Stenstroem P.: Priority inheritance protocols: the worst case execution-time problem: overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. 7(3), 1\u201353 (2008)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"156_CR40","volume-title":"Bernstein Polynomials","author":"G. Lorentz","year":"1953","unstructured":"Lorentz G.: Bernstein Polynomials. University of Toronto Press, Toronto (1953)"},{"issue":"6","key":"156_CR41","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1016\/0167-8396(91)90031-6","volume":"8","author":"T. Sauer","year":"1991","unstructured":"Sauer T.: Multivariate Bernstein polynomials and convexity. Comput. Aided Geom. Des. 8(6), 465\u2013478 (1991)","journal-title":"Comput. Aided Geom. Des."},{"key":"156_CR42","unstructured":"Wolfram Research: Mathemathica 5.2. www.wolfram.com"},{"key":"156_CR43","doi-asserted-by":"crossref","unstructured":"Carnevali, L., Ridi, L., Vicario, E.: Stochastic fault trees for cross-layer power management of wsn monitoring systems. In: Proceedings of the IEEE Conference on Emerging Technologies and Factory Automation (ETFA) (2009)","DOI":"10.1109\/ETFA.2009.5347071"},{"key":"156_CR44","doi-asserted-by":"crossref","unstructured":"Bucci, G., Carnevali, L., Vicario, E.: A tool supporting evaluation of non-markovian fault trees. In: Proceedings of the 5th Int. Conf. on Quant. Evaluation of Sys. (QEST \u201905) (2008)","DOI":"10.1109\/QEST.2008.46"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0156-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0156-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0156-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:26Z","timestamp":1559114726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0156-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5,9]]},"references-count":44,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["156"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0156-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5,9]]}}}