After two decades of research on superimpositions, aspects, and complex event notations, I suggest several basic principles for specifying and formally verifying modules using such cross-cutting notations. These principles can also be applicable for emerging applications and new modularization constructs.

First, it is essential to find a clean semantic definition for the construct, e.g., viewing aspects as a system transformer. This leads to the need for specification as the relation between “before” and “after” applying the construct. Specifications need also to carefully include the context in order to be verifiable. Verification needs to be done for generic contexts, in advance of use in applications, and must deal with interferences among such complex modules. Finally, existing automatic tools and results from formal methods can and should be adapted to new modularity constructs.

After illustrating these ideas for aspects and complex events, I show their relevance for additional domains. As one example, autonomous systems, such as lunar rovers, need to be self-stabilizing under arbitrary faults (e.g., when cosmic rays corrupt small but key parts of computer memory). Such faults can throw the system to an otherwise “impossible” state, and a self-stabilizing module needs to then return the system to normal operation without unnecessarily disturbing parts of the system that still are functioning correctly. Other examples include augmenting systems to analyze and optimize power consumption, and modeling internet or cloud security with several modules that simulate attacks, detect an ongoing attack, and/or prevent incursions or disruptions of service.

Bio

Shmuel Katz is an Emeritus Professor in the Computer Science Department at the Technion—Israel Institute of Technology. He joined the Technion in 1981, helped develop and lead the Software Engineering degree track, and directed the Systems and Software Development Lab. His Sabbaticals and extended visits include UC Berkeley, Carnegie-Mellon University, University of Lancaster, University of Twente, Tampere University of Technology, and the University of Texas at Austin.

He has written over 100 journal and conference papers on using formal methods to improve software quality, modularity, and reliability. His early work focused on automatic generation of invariants, multiparty interactions for distributed programming, fault tolerance using self-stabilizing systems, and verifying properties such as database serializability using convenient execution sequences. Since 2000 his work has centered on specification and formal verification for aspect-oriented and event-driven programming. He was Editor-in-Chief of the Transactions on Aspect-Oriented Software Development from 2009 to 2011.

Shmuel Katz is an Emeritus Professor in the Computer Science Department at the Technion—Israel Institute of Technology. He joined the Technion in 1981, and helped develop and lead the Software Engineering degree track, and directed the Systems and Software Development Lab. His Sabbaticals and extended visits include UC Berkley, Carnegie-Mellon University, University of Lancaster, Technical Institute of Twente, Technical Institute of Tampere, and the University of Texas at Austin.

He has written over 100 journal and conference papers on using formal methods to improve software quality, modularity, and reliability. His early work focused on automatic generation of invariants, multiparty interactions for distributed programming, fault tolerance using self-stabilizing systems, and verifying properties such as database serializability using convenient execution sequences. Since 2000 his work has centered on specification and formal verification for aspect-oriented and event-driven programming. He was Editor-in-Chief of the Transactions on Aspect-Oriented Software Development from 2009-2011.