Monitoring probabilistic properties

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Monitoring probabilistic properties

Full text

Pdf (506 KB)

Source

Foundations of Software Engineering archive
Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering on European software engineering conference and foundations of software engineering symposium table of contents

Amsterdam, The Netherlands

SESSION: Software quality & performance table of contents

Pages 183-192

Year of Publication: 2009

ISBN:978-1-60558-001-2

Authors

Lars Grunske	Swinburne University of Technology, Hawthorn, Australia
Pengcheng Zhang	Southeast University, Nanjing, China

Sponsors

ACM: Association for Computing Machinery
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 32, Downloads (12 Months): 75, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1595696.1595724 What is a DOI?

ABSTRACT

Monitoring allows for checking if a system fulfils its requirements at runtime. This is required for quality assurance purposes. Currently several approaches exist to monitor standard and timing properties. However, a current challenge is to provide a comprehensive approach for monitoring probabilistic properties, as they are used to formulate performance, reliability, safety, and availability requirements. The main problem of these probabilistic properties is that there is no binary acceptance condition. To overcome this problem, this paper describes a monitoring approach called ProMo that is based on acceptance sampling and sequential hypothesis testing. This approach is validated based on several experiments that have been performed on an example system which provides medical assistance in remote areas.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	A. Aziz, K. Sanwal, V. Singhal, and R. K. Brayton. Verifying continuous time markov chains. In R. Alur and T. A. Henzinger, editors, Proc. 8th International Conference on Computer Aided Verification, CAV 96, volume 1102 of LNCS, pages 269--276. Springer, 1996.
	2	A. Aziz, V. Singhal, and F. Balarin. It usually works: The temporal logic of stochastic systems. In P. Wolper, editor, Proc. 7th International Conference on Computer Aided Verification, CAV 95, volume 939 of LNCS, pages 155--165. Springer, 1995.
	3	C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng, 29(6):524--541, 2003.
	4	C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time markov chains. In J. C. M. Baeten and S. Mauw, editors, Proc. 10th International Conference on Concurrency Theory, CONCUR 99, volume 1664 of LNCS, pages 146--161. Springer, 1999.
	5	L. Baresi, D. Bianculli, C. Ghezzi, S. Guinea, and P. Spoletini. A timed extension of WSCoL. In IEEE International Conference on Web Services, pages 663--670, 2007.
	6	H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-based runtime verification. Proc. 5th International Conference Verification, Model Checking, and Abstract Interpretation, VMCAI, volume 2937 of LNCS, pages 44--57. Springer, 2004.
	7	A. Bertolino, G. D. Angelis, L. Frantzen, and A. Polini. Model-based generation of testbeds for web services. In K. Suzuki, T. Higashino, A. Ulrich, and T. Hasegawa, editors, Proc. 20th IFIP TC 6/WG 6.1 International Conference, TestCom 2008, volume 5047 of LNCS, pages 266--282. Springer, 2008.
	8	A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In P. S. Thiagarajan, editor, Proc. of the 15th Conference on Foundations of Software Technology and Theoretical Comp. Science, FSTTCS 95, volume 1026 of LNCS, pages 499--513. Springer, 1995.
	9	K. Chan, I. Poernomo, H. W. Schmidt, and J. Jayaputera. A model-oriented framework for runtime monitoring of nonfunctional properties. In Proc. of the 1st Int. Conf. on the Quality of Software Architectures, QoSA 2005, volume 3712 of LNCS, pages 38--52. Springer, 2005.
	10	K. S. M. Chan, J. Bishop, J. Steyn, L. Baresi, and S. Guinea. A fault taxonomy for web service composition. In E. D. Nitto and M. Ripeanu, editors, Workshop on Engineering Service-Oriented Applications (WESOA07), volume 4907 of LNCS, pages 363--375. Springer, 2007.
	11	L. A. Clarke and D. S. Rosenblum. A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Software Engineering Notes, 31(3):25--37, 2006.
	12	R. Colvin, L. Grunske, and K. Winter. Probabilistic timed behavior trees. In J. Davies and J. Gibbons, editors, Proceedings of the International Conference on Integrated Formal Methods (IFM 2007), volume 4591 of LNCS, pages 156--175. Springer-Verlag, 2007.
	13	M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In Proc. 21st International Conference on Software Engineering, ICSE 99, pages 411--420. IEEE Comp. Society/ACM Press, 1999.
	14	I. Epifani, C. Ghezzi, R. Mirandola, and G. Tamburrelli. Model evolution by run-time parameter adaptation. In S. Fickas, J. Atlee, and P. Inverardi, editors, Proc. 31st International Conference on Software Engineering, ICSE 2009, volume 4839, pages 111--121. IEEE, 2009.
	15	S. Gallotti, C. Ghezzi, R. Mirandola, and G. Tamburrelli. Quality prediction of service compositions through probabilistic model checking. In Proc. 4th International Conference on the Quality of Software-Architectures, QoSA 2008, volume 5281 of LNCS, pages 119--134. Springer, 2008.
	16	V. Gruhn and R. Laue. Patterns for timed property specifications. Electr. Not. Theor. Comp. Sci, 153(2):117--133, 2006.
	17	L. Grunske. Specification patterns for probabilistic quality properties. In Robby, editor, 30th International Conference on Software Engineering (ICSE 2008), pages 31--40. ACM, 2008.
	18	L. Grunske, R. Colvin, and K. Winter. Probabilistic Model-Checking Support for FMEA. In Proc. 4th International Conference on the Quantitative Evaluation of Systems, QEST 07, pages 119--128. IEEE Computer Society, 2007.
	19	H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512--535, 1994.
	20	A. Keller and H. Ludwig. Defining and monitoring service-level agreements for dynamic e-business. In Proceedings of the 16th Systems Administration Conference (LISA-02), pages 189--204, Berkeley, CA, 2002. USENIX Association.
	21	S. Konrad and B. H. C. Cheng. Real-time specification patterns. In G.-C. Roman, W. G. Griswold, and B. Nuseibeh, editors, 27th Int. Conf. on Software Engineering, ICSE 05, pages 372--381. ACM, 2005.
	22	M. Z. Kwiatkowska. Model checking for probability and time: from theory to practice. In Proceedings of the 18th Annual IEEE Syposium on Logic in Computer Science, LICS 03, pages 351--360, Los Alamitos, CA, June 22--25 2003. IEEE Computer Society.
	23	M. Z. Kwiatkowska, G. Norman, D. Parker, and J. Sproston. Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design, 29(1):33--78, 2006.
	24	K. Mahbub and G. Spanoudakis. Monitoring WS-agreements: An event calculus-based approach. In L. Baresi and E. D. Nitto, editors, Test and Analysis of Web Services, pages 265--306. Springer, 2007.
	25	D. Mukherjee, P. Jalote, and M. G. Nanda. Determining QoS of WS-BPEL Compositions. In A. Bouguettaya, I. KrÄuger, and T. Margaria, editors, 6th International Conference on Service-Oriented Computing - ICSOC 2008, volume 5364 of LNCS, pages 378--393, 2008.
	26	B. Paech and T. Wetter. Rational quality requirements for medical software. In Robby, editor, 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008, pages 633--638. ACM, 2008.
	27	A. Pretschner, M. Broy, I. H. Krüuger, and T. Stauner. Software engineering for automotive systems: A roadmap. In L. C. Briand and A. L. Wolf, editors, International Conference on Software Engineering, ICSE 2007, Future of Software Engineering, pages 55--71, 2007.
	28	F. Raimondi, J. Skene, and W. Emmerich. Efficient online monitoring of web-service SLAs. In SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, pages 170--180, New York, NY, USA, 2008. ACM Press.
	29	U. Sammapun, I. Lee, O. Sokolsky, and J. Regehr. Statistical runtime checking of probabilistic properties. In O. Sokolsky and S. Tasiran, editors, Runtime Verification, 7th International Workshop, RV 2007, volume 4839 of LNCS, pages 164--175. Springer, 2007.
	30	K. Sen, M. Viswanathan, and G. Agha. Statistical model checking of black-box probabilistic systems. In R. Alur and D. Peled, editors, Proc. 16th International Conference Computer Aided Verification, CAV 04, volume 3114 of LNCS, pages 202--215. Springer, 2004.
	31	K. Sen, M. Viswanathan, and G. Agha. On statistical model checking of stochastic systems. In K. Etessami and S. K. Rajamani, editors, Proc. 17th International Conference Computer Aided Verification, CAV 05, volume 3576 of LNCS, pages 266--280. Springer, 2005.
	32	J. Skene, A. Skene, J. Crampton, and W. Emmerich. The monitorability of service-level agreements for application-service provision. In V. Cortellessa, S. Uchitel, and D. Yankelevich, editors, Proceedings of the 6th International Workshop on Software and Performance, WOSP 2007, pages 3--14. ACM, 2007.
	33	T. Suto, J. T. Bradley, and W. J. Knottenbelt. Performance trees: A new approach to quantitative performance specification. In 14th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2006), pages 303--313. IEEE Computer Society, 2006.
	34	A. Wald. Sequential tests of statistical hypotheses. The Annals of Mathematical Statistics, 16(2):117--186, 1945.
	35	H. L. S. Younes. Probabilistic verification for "black-box" systems. In K. Etessami and S. K. Rajamani, editors, Computer Aided Verification, 17th International Conference, CAV 2005, volume 3576 of LNCS, pages 253--265. Springer, 2005.
	36	H. L. S. Younes. Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, PhD thesis, Computer Science Department, Carnegie Mellon University, Pittsburgh, Pennsylvania. CMU-CS-05-105., 2005.
	37	H. L. S. Younes. Error control for probabilistic model checking. In E. A. Emerson and K. S. Namjoshi, editors, 7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006, volume 3855 of LNCS, pages 142--156. Springer, 2006.
	38	H. L. S. Younes and R. G. Simmons. Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput., 204(9):1368--1409, 2006.
	39	P. Zhang, B. Li, and M. Sun. Extending PSC for monitoring the timed properties in composite services. In Proc. of 15th Asia-Pacific Software Engineering Conference (APSEC 2008), pages 335--342, Beijing, China, 2008. IEEE Computer Society Press.
	40	P. Zhang, B. Li, and M. Sun. A timed extension of property sequence chart. In 11th IEEE High Assurance Systems Engineering Symposium(HASE'08), pages 197--206, Nanjing, China, 2008. IEEE Computer Society.
	41	T. Zheng, C. M. Woodside, and M. Litoiu. Performance model estimation and tracking using optimal filters. IEEE Trans. Software Eng, 34(3):391--406, 2008.