Engineering the usability of visual formalisms: a case study in real time logics

ABSTRACT

A visual formalism for the presentation of a real time logic is introduced, motivated, and evaluated.The visual formalism has been designed following a user-centered usability engineering process, targeted to the students of higher education courses in software engineering. On the one hand, heuristic design was applied to maximize consistency, i.e. to minimize the complexity of the visual metaphor mapping textual sentences to the visual representation. On the other hand, individual metaphoric assumptions were defined by prototyping and exposing alternative graphical representations to a representative sample of the target community of expected users.The resulting notation has been implemented within an interactive syntax-directed editor which integrates the visual presentation with the conventional textual notation. The editor has been used to carry out a competitive user-based evaluation of the usability of textual and visual representations, by carrying out a readability test on a larger sample of representative end-users.

REFERENCES

• 1: James F. Allen, Maintaining knowledge about temporal intervals, Communications of the ACM, v.26 n.11, p.832-843, Nov. 1983 [doi>10.1145/182.358434]
• 2: R. Alur, C. Courcoubetis, D. Dill, "Model-Checking for Real-Time Systems," Proc. 5th Symp. on Logic in Computer Science, Philadelphia, June 1990.
• 3: Rajeev Alur , Thomas A. Henzinger, Logics and Models of Real Time: A Survey, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.74-106, June 03-07, 1991
• 4: Rajeev Alur , Thomas A. Henzinger, Real-time logics: complexity and expressiveness, Information and Computation, v.104 n.1, p.35-77, May 1993 [doi>10.1006/inco.1993.1025]
• 5: Bernard Berthomieu , Michel Diaz, Modeling and Verification of Time Dependent Systems Using Time Petri Nets, IEEE Transactions on Software Engineering, v.17 n.3, p.259-273, March 1991 [doi>10.1109/32.75415]
• 6: Giacomo Bucci , Enrico Vicario, Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets, IEEE Transactions on Software Engineering, v.21 n.12, p.969-992, December 1995 [doi>10.1109/32.489073]
• 7: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 8: B. Dasarathy, "Timing Constraints of Real-Time Systems: Constructs for Expressing Them, Methods for Validating Them," IEEE Transactions on Software Engineering, Vol.11, No.1, Jan. 1985.
• 9: A. Del Bimbo , L. Rella , E. Vicario, Visual specification of branching time temporal logic, Proceedings of the 11th International IEEE Symposium on Visual Languages, p.61, September 05-09, 1995
• 10: D. L. Dill, Timing assumptions and verification of finite-state concurrent systems, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.197-212, February 1990, Grenoble, France
• 11: David Harel, On visual formalisms, Communications of the ACM, v.31 n.5, p.514-530, May 1988 [doi>10.1145/42411.42414]
• 12: Eben M. Haber , Yannis E. Ioannidis , Miron Livny, Foundations of visual metaphors for schema display, Journal of Intelligent Information Systems, v.3 n.3-4, p.263-298, July 1994 [doi>10.1007/BF00962239]
• 13: G. Kutty, Y. S. Ramakrishna, L. E. Moser, L. K. Dillon, P. M. Melliar Smith, "A Graphical Interval Logic Toolset for Verifying Concurrent Systems," Proc. of the fourth Workshop on Computer Aided Verification, Montreal, Canada, June 1992.
• 14: Leslie Lamport, TLA in Pictures, IEEE Transactions on Software Engineering, v.21 n.9, p.768-775, September 1995 [doi>10.1109/32.464544]
• 15: G. Kutty, L. K. Dillon, L. E. Moser, P. M. Melliar Smith, Y. S. Ramakrishna, "Visual Tools for Temporal reasoning," Proc. VL'93, Bergen, Norway, 1993.
• 16: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 17: L. E. Moser , Y. S. Ramakrishna , G. Kutty , P. M. Melliar-Smith , L. K. Dillon, A graphical environment for the design of concurrent real-time systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.1, p.31-79, Jan. 1997 [doi>10.1145/237432.237438]
• 18: Jakob Nielsen, Usability Engineering, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1993
• 19: Jakob Nielsen, Iterative User-Interface Design, Computer, v.26 n.11, p.32-41, November 1993 [doi>10.1109/2.241424]
• 20: Jakob Nielsen, The Usability Engineering Life Cycle, Computer, v.25 n.3, p.12-22, March 1992 [doi>10.1109/2.121503]
• 21: A. Pnueli, "The Temporal Logic of Program," Proc. 18th Annual Symposium on Foundations of Computer Science, pp. 46--57, IEEE Comp. Soc. Press, 1977.
• 22: John A. Stankovic , Krithi Ramamritham, What is predictability for real-time systems?, Real-Time Systems, v.2 n.4, p.247-254, Nov. 1990 [doi>10.1007/BF01995673]
• 23: John A. Stankovic, Misconceptions About Real-Time Computing: A Serious Problem for Next-Generation Systems, Computer, v.21 n.10, p.10-19, October 1988 [doi>10.1109/2.7053]
• 24: Edward Tufte, Envisioning information, Graphics Press, Cheshire, CT, 1990
• 25: J. Xu , D. L. Parnas, On Satisfying Timing Constraints in Hard-Real-Time Systems, IEEE Transactions on Software Engineering, v.19 n.1, p.70-84, January 1993 [doi>10.1109/32.210308]

INDEX TERMS

Keywords:
computer aided verification, real time logics, usability engineering, visual formalisms