Hello everyone,
I am looking for some advice regarding TLA+, in particular in evaluating if could be the right tool for my problem. My experience with TLA+ is quite limited so I figured I'd ask people with more experience for advice.
On my current assignment, I am working with Dynamics 365 CE system. This system allows to develop a plug-in with custom business logic to modify or augment the standard behavior of the platform. Plug-ins are essentially handlers for events fired by Dynamics 365 Customer Engagement . You can subscribe, or register, a plug-in to a known set of events to have your code run when the event occurs.
For example, when user is creating an Opportunity entity record in the system, the system determines the Default Price List for the current user and sets this value on the newly created record.
Our implementation relies heavily on these customizations, i.e. there lot of plug-ins in the system with business logic that supports pricing and financing use cases, approval workflows, etc.
My main concern is mainly these points:
- Currently, we have no overview about the chain of events happening in the system. Imagine situations like a certain plug-in logic being fired twice resulting in wrong calculations as an end result, infinite loops, unnecessary wait times for some of the events etc.
- Testability of the system in general. The plug-in code is tested by unit test, but these won't test the behavior of the plug-in within the platform. We developed a set of Integration tests, that exercises the plug-in logic by invoking the events that should trigger the plug-in logic. From the example I've given above, the test will arrange a particular system state, send a Create request for Opportunity entity record and assert if the Price List value matches the expected Default Price List value hence verifying the system behavior.
- The plug-in code turned into a big ball of mud. The developers are afraid to touch some of the plug-in code with fear to introduce bugs when developing new features for critical business logic related to pricing or financing. The Integration tests I mentioned above provide a safety net, but they don't guarantee that in certain edge cases a bug hasn't slipped into the system.
What I strive for is to really gain confidence about the system behavior and avoid subtle bugs. From my perspective, the system could be viewed as black box where the events transform the system from one state to another. Ideally we would like to check that the state of the system after an event is "correct" as a result of the plug-in logic.
Does someone see a possibility that TLA+ could be a useful tool in this context? Maybe some tools which would support property-based testing would be more appropriate in this case, but I am still searching...
So far, I only experimented a bit with TLA+ as interesting pastime project. I found it both interesting and powerful, but it never occurred to me to use it as part of my current role as I simply thought that it is suited to solve problems in a completely different domain.
I wish a knew about it while is writing my diploma thesis on network coding for distributed storage systems though. It would save me some time.
Thank you for you opinions.
Martin