| |
 |
|
|
Lam, Vitus
The University of Hong Kong
Hong Kong, Hong Kong
|
|
|
 |
|
|
| |
| |
|
Date Reviewed |
|
| |
1 - 8 of 8
reviews
|
|
|
|
|
|
|
|
Handbook of model checking
Clarke E., Henzinger T., Veith H., Bloem R., Springer International Publishing, New York, NY, 2018. 1210 pp. Type: Book (978-3-319105-74-1)
Due to the proliferation and pervasiveness of hardware and software entities in everyday life, ascertaining their trustworthiness is of paramount importance. Model checking is a logic-based approach that determines whether the abstract...
|
May 20 2019 |
|
|
|
|
|
|
Time patterns for process-aware information systems
Lanz A., Weber B., Reichert M. Requirements Engineering 19(2): 113-141, 2014. Type: Article
Employing patterns for capturing solutions to recurring problems is an idea that stems from the field of architecture. Within the context of business process management (BPM), a wide spectrum of patterns has been identified and documen...
|
Nov 19 2014 |
|
|
|
|
|
|
Modeling and enacting complex data dependencies in business processes
Meyer A., Pufahl L., Fahland D., Weske M. BPM 2013 (Proceedings of the 11th International Conference on Business Process Management, Beijing, China, Aug 26-30, 2013) 171-186, 2013. Type: Proceedings
Business process management (BPM) is an interdisciplinary field that works to advance both foundational theories and methodologies for constructing and analyzing business process models in a cross-organizational setting. In the BPM are...
|
Jan 20 2014 |
|
|
|
|
|
|
Bounded model-checking of discrete duration calculus
Zu Q., Zhang M., Zhu J., Zhan N. HSCC 2013 (Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Philadelphia, PA, Apr 8-11, 2013) 213-222, 2013. Type: Proceedings
In the model-checking community, asserting the soundness of a finite-state model is achieved by verifying the model against appropriate mathematical specifications. The duration calculus is an interval temporal logic for defining speci...
|
Oct 10 2013 |
|
|
|
|
|
|
Abstractions for validation in action
de Caso G., Braberman V., Garbervetsky D., Uchitel S. SFM 2012 (Proc. of the 12th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, Bertinoro, Italy, Jun 18-23, 2012) 192-218, 2012. Type: Proceedings
Abstraction is a software engineering technique for constructing a model by capturing the essential features and properties of the respective real-world system. Determining which irrelevant details to omit and the appropriate level of ...
|
Nov 16 2012 |
|
|
|
|
|
|
Compositional model checking of software product lines using variation point obligations
Liu J., Basu S., Lutz R. Automated Software Engineering 18(1): 39-76, 2011. Type: Article
A prominent challenge in model checking lies in alleviating the state explosion problem of complicated systems. Compositional model checking is a mathematically founded technique for reasoning about complex systems by employing a modul...
|
Jul 6 2011 |
|
|
|
|
|
|
Type inference and strong static type checking for PROMELA
Donaldson A., Gay S. Science of Computer Programming 75(11): 1165-1191, 2010. Type: Article
The formal methods domain uses model checking as a rigorous technique for analyzing the validity of systems in a disciplined manner. The SPIN model checker is a software tool that mechanically verifies the abstract representation of a ...
|
Nov 8 2010 |
|
|
|
|
|
|
 Formal verification of AADL behavior models: a feasibility investigation
Liu H., Gluch D. ACM-SE 47 (Proceedings of the 47th Annual Southeast Regional Conference, Clemson, SC, Mar 19-21, 2009) 1-6, 2009. Type: Proceedings
In light of the ubiquity and ever-increasing complexity of real-time embedded systems, the development of a disciplined approach to engineer these often safety-critical and mission-critical systems has become a necessity. The Society o...
|
Aug 28 2009 |
|
|
|
|
|
| |
|
|
| |
|
|
